diff options
| author | filliatr | 1999-09-19 14:17:35 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-19 14:17:35 +0000 |
| commit | 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 (patch) | |
| tree | 5a5a73ee8770cba524b8c24892f709a308e9ab3b /kernel/inductive.mli | |
| parent | 5393ee683be9e19ab25888925f561ea4f4b1dddb (diff) | |
- un effort sur la doc (ocamlweb)
- module Nametab
- module Impargs
- correction bug : Parameter id : t => vérification que t est bien un type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a08136424a..d0dee30b92 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -64,6 +64,9 @@ type mutual_inductive_entry = { mind_entry_finite : bool; mind_entry_inds : (identifier * constr * identifier list * constr) list } +(*s The different kinds of errors that may result of a malformed inductive + definition. *) + type inductive_error = | NonPos of int | NotEnoughArgs of int @@ -76,6 +79,9 @@ type inductive_error = exception InductiveError of inductive_error +(*s The following functions are utility functions to check and to + decompose a declaration. *) + (* [mind_check_names] checks the names of an inductive types declaration i.e. that all the types and constructors names are distinct. It raises an exception [InductiveError _] if it is not the case. *) @@ -92,5 +98,4 @@ val mind_extract_and_check_params : val mind_extract_params : int -> constr -> (name * constr) list * constr - val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit |