The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Yes, this is a bug (an "anomaly" is always a bug worth reporting, though occasionally the bug is just "there should be a real error message here"), but it doesn't seem to occur in Coq 8.6; your "unshelve refine" fails.

On Fri, Feb 10, 2017 at 11:05 AM Tom Hirschowitz <tom.hirschowitz AT univ-smb.fr> wrote:

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.