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.