The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/10/2017 12:35 PM, Jason Gross wrote:

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.

This is probably https://coq.inria.fr/bugs/show_bug.cgi?id=5122

Note that cases there that produced the bug in pre-release 8.6 versions now fail in released 8.6 before producing the bug as well.

-- Jonathan

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.