The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Adam,

  yes, there is an incompatible change in 8.3: you have
to declare that [A] is generalizable using the
[Generalizable Variables A.] vernacular command (documented 
in the reference manual).

-- Matthieu

Le 20 sept. 2010 à 14:28, Adam Megacz a écrit :

> 
> (* The script below works with 8.2pl3 but reports "Error: Unbound and
> * ungeneralizable variable A" with 8.3rc1 *)
> 
> Inductive list (A:Type) : Type :=
>  | nil : list A
>  | cons : A -> list A -> list A.
> Implicit Arguments nil [A].
> Implicit Arguments cons [A].
> Infix "::" := cons (at level 60, right associativity).
> Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = 
> (a::b) -> False.
>  intros.
>  induction b.
>  inversion H.
>  inversion H. apply IHb in H2.
>  auto.
>  Defined.
> 
> 
>