diff options
| author | herbelin | 2000-05-18 08:19:49 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-18 08:19:49 +0000 |
| commit | 57740cb8ed713e5e79e441a31176955fd94220fa (patch) | |
| tree | 91951b90b9395c0d23454e6f1bcfe00061f533aa /kernel/indtypes.mli | |
| parent | 1e07202f283a6e8358378ffe4e945abd157b079c (diff) | |
Ajouts des causes d'erreur de Indrec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@446 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index e955f6009e..505ea1d955 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -5,7 +5,7 @@ open Names open Univ open Term -open Inductive +open Constant open Environ (*i*) @@ -14,6 +14,7 @@ open Environ definition. *) type inductive_error = + (* These are errors related to inductive constructions in this module *) | NonPos of name list * constr * constr | NotEnoughArgs of name list * constr * constr | NotConstructor of name list * constr * constr @@ -22,6 +23,10 @@ type inductive_error = | SameNamesConstructors of identifier * identifier | NotAnArity of identifier | BadEntry + (* These are errors related to recursors building in Indrec *) + | NotAllowedCaseAnalysis of bool * sorts * inductive + | BadInduction of bool * identifier * sorts + | NotMutualInScheme exception InductiveError of inductive_error |