coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Recursive call to ... had not enough arguments

From: David Monniaux <David.Monniaux AT ens.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Recursive call to ... had not enough arguments
Date: Thu, 31 Mar 2005 11:16:02 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

I did a complex proof by 3 nested inductions, and when I do Qed, I'm getting:
Recursive call to inductive_predicate had not enough arguments

What does that mean?

Regards,
-- DM

[Coq-Club] Recursive call to ... had not enough arguments, David Monniaux