The Coq mailing list

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

Ah, right, thanks to both of you. (And sorry for not looking directly
into the bug tracker, I confess I trusted google...)

Tom

> 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.
>>>