The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

On Tuesday 28 June 2011 17:59:59 Randy Pollack wrote:
> but this is rejected: "Error: Unbound and ungeneralizable variable A".
> 
> What am I misunderstanding?

You need to declare
Generalizable All Variables.
or only the ones you need, see 
http://coq.inria.fr/refman/Reference-Manual004.html#@command88
-- 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France