mach et himsg; typage sans extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@21 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 41 insertions, 2 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 32d844e9a7..d3022c5697 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -2,11 +2,50 @@
 (* $Id$ *)
 
 open Names
+open Term
+open Sign
 
-type mind_entry
+type recarg = 
+  | Param of int 
+  | Norec 
+  | Mrec of int 
+  | Imbr of section_path * int * (recarg list)
 
-type mutual_inductive_body
+type mutual_inductive_packet = {
+  mind_consnames : identifier array;
+  mind_typename : identifier;
+  mind_lc : constr;
+  mind_stamp : name;
+  mind_arity : typed_type;
+  mind_lamexp : constr option;
+  mind_kd : sorts list;
+  mind_kn : sorts list;
+  mind_listrec : (recarg list) array;
+  mind_finite : bool }
+
+type mutual_inductive_body = {
+  mind_kind : path_kind;
+  mind_ntypes : int;
+  mind_hyps : typed_type signature;
+  mind_packets : mutual_inductive_packet array;
+  mind_singl : constr option;
+  mind_nparams : int }
 
 type mutual_inductive_entry = section_path * mutual_inductive_body
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
+
+type mind_specif = {
+  mis_sp : section_path;
+  mis_mib : mutual_inductive_body;
+  mis_tyi : int;
+  mis_args : constr array;
+  mis_mip : mutual_inductive_packet }
+
+val mis_ntypes : mind_specif -> int
+val mis_nconstr : mind_specif -> int
+val mis_nparams : mind_specif -> int
+val mis_kd : mind_specif -> sorts list
+val mis_kn : mind_specif -> sorts list
+val mis_recargs : mind_specif -> (recarg list) array array
+