The Coq mailing list

[Tom Hirschowitz <tom.hirschowitz AT univ-smb.fr>]

Hi all,

The little proof below fails on exact (...) with

Anomaly: cannot define an evar twice. Please report.

But it does go through using apply instead of exact.

Is this a bug?

Thanks,
Tom

PS: the code grew out of an attempt at finding an efficient way to program 
the equivalent

Definition trivial' A (a : A) (F : el (Typ A) a) : El a = F :=
  match F with El _ => eq_refl end.

from the tactic language (in a more complex setting, of course). 

I'd be grateful for any hints about this too :)

---------------------------------------------------


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive typ : Type -> Type := Typ : forall T, typ T.
Inductive el : forall A, typ A -> A -> Type :=
  El : forall A (a : A), el (Typ A) a.

Definition trivial A (a : A) (F : el (Typ A) a) : El a = F.
  unshelve refine (@el_rect _ _ A (Typ A) a F).
  clear A a F.
  intros A X a F.
  unshelve refine ((@typ_rect (fun A' X' => (forall a' : A', el X' a' -> 
Type)) _ A X) a F).
  clear A X a F.
  intros A a F.
  exact (El a = F).
  simpl.
  reflexivity.
Defined.