The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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