The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Anomalies are always bugs on the Coq side, they are always worth reporting. The bug tracker is to be found here : http://www.lix.polytechnique.fr/coq/bugs/  (your bug seems to be new)

As an aside, you seem to be right about the source of the bug, here is a minimal example :
Definition X (A := Type) : A := nat.

The following doesn't cause an error though:
Definition Type1 := Type.

Definition X (A := Type1) : A := nat.

On 29 May 2012 18:20, Jason Gross <jasongross9 AT gmail.com> wrote:

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.

Require Import Eqdep.

Import Eq_rect_eq.

Definition cast a b (p : a = b) : a -> b.

  intro; rewrite <- p; assumption.

Defined.

Implicit Arguments cast [a b].

Lemma cast_nop T (p : T = T) (a : T) : cast p a = a.

  unfold cast; rewrite <- eq_rect_eq; reflexivity.

Qed.

Lemma cast_app_nop A (F := A -> Type) (pF : F = F) (pA : A = A) (f : F) (a : A) : ((cast pF f) (cast pA a)) = f a.

  unfold cast; repeat (rewrite <- eq_rect_eq); reflexivity.

Qed.

-Jason

P.S. I also get it if I replace the proof and the [Qed.] with [admit.]