From 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Sun, 19 Sep 1999 14:17:35 +0000
Subject:  - 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
---
 kernel/inductive.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/inductive.mli')

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
-- 
cgit v1.2.3