The Coq mailing list

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

You need to
Require Program.
or just
Require Program.Equality.

Hope this helps,
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France


On Monday 14 November 2011 09:51:00 Altenkirch Thorsten wrote:
> Hi,
> 
> I am using
> Coq 8.3pl2 (April 2011)
> 
> When I try to use
> 
> dependent induction
> 
> I get the error message
> 
> Toplevel input, characters 28-37:
> Syntax error: 'generalize_eqs_vars' or 'generalize_eqs' or 'rewrite' or
> 'simple' 'inversion' expected after 'dependent' (in
> [tactic:simple_tactic]).
> 
> Which sounds like it doesn't know about dependent induction. What is wrong?