This crashes Coq 8.4pl2...

gistfile1.coq

Require Import Le.

(* We shouldn't really need the return clause here, but Coq 8.4pl2
will crash without it... *)

Definition test (i : nat) (x : {n : nat | n <= i}) : nat :=
  match x with
  | exist O _ => 0
  | exist (S x') p => 
    match i (* return (S x' <= i) -> nat *) with
    | O => fun p => except (le_Sn_0 x' p)
    | S i' => fun _ => 0
    end p
  end.