The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

dimitrisg7 wrote:
> I would like to get "Var" given by Hypothesis e in the following example.
>
>  e : exists v : Var, f_expr_IL v = nth j el dE 
>   ============================
>    Var
>
> Writing "elim e" I get the error:
>
> Toplevel input, characters 9-15:
> Error: Cannot find the elimination combinator ex_rec, the elimination of the
> inductive definition ex on sort Set is probably not allowed
>
> The problem is "Var" is an inductive definition of type "Type". Giving "Var"
> type "Prop" solves the problem for me. Is there a way to get v without
> turning Var's type to Prop?
>   

I hope not, as that would indicate a foundational bug in Coq.  You've 
marked [e] as a proof, and Gallina's type system is supposed to prevent 
any "information flow" from proofs to non-proofs.  Maybe you want a 
[sig] type instead of an [ex] type for [e].

P.S.: Please don't reply to your old threads with new, unrelated 
questions.  It leads to not-especially-helpful message subjects.