The Coq mailing list

[Sylvain Dailler <sylvain.dailler AT ens-lyon.fr>]

Dear Coq users, 

I would like to use the inversion tactic in the
sort Prop. But this tactic has not the same behavior as in Set. I don't
understand why.
My problem can be summarized with this little example :

Variable A : Set.

Variable plus : A -> A -> A.
Infix "+" := plus.
Variable A0 : A.
Variable A1 : A.

Inductive example : A -> A -> Prop := 
| example0 : forall x y, example x (y + A1).



Lemma example_context : forall x, example x A0 -> False.
Proof.
intros x Hpipo.
inversion Hpipo.
(*now look at the context with A : Prop*)
Admitted. 


Now,
if I change "Variable A : Set." into "Variable A : Prop.", the context
generated by the inversion tactic is not the same. This hypothesis
disappeared :

"H1 : y + A1 = A0"

I would like to know why contexts are different. I don't think I am doing anything wrong with the Prop sort.

Do you know where I can find the code of the inversion tactic ?