The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 29 mai 2012 à 18:20, Jason Gross a écrit :

> Hi,
> When I execute the last [Qed] in the following code, I get 
>   Anomaly: Cannot take the successor of a non variable universe:
>   (maybe a bugged tactic).
>   Please report.
> I'm pretty sure this is Coq telling me that my [F := A -> Type] is bad 
> (though I'm not sure exactly what's wrong with it).  Is this worth 
> reporting, and, if so, where should I report it to?  Thanks.

<snip/>

Hi Jason, thanks for the report. Indeed it is a minor bug in the treatment of 
universes in binders before the :.
The following works:

Lemma cast_app_nop A : forall (F := A -> Type) (pF : F = F) (pA : A = A) (f : 
F) (a : A), ((cast pF f) (cast pA a)) = f a.
Prooof. intros;  unfold cast; repeat (rewrite <- eq_rect_eq); reflexivity. 
Qed.
-- Matthieu