The Coq mailing list

["Stefan Monnier" <monnier+lists/coq AT rum.cs.yale.edu>]

> >   (iptr r n)=(iptr ?2570 ?2571)
> 
> Try:
> Lemma xeqx: (A:Set)(x:A)(x=x).
> Proof.
> Reflexivity.
> Qed.

I believe the above is equivalent to

   Definition xeqx := refl_equal.

> And use "Apply xeqx.". I noticed that kind of things helps with
> metavariables.

It makes no difference: I also get `Error: w_Unify'.


        Stefan