Ajout des fonctions de formation du 'case_info'; Suppression de make_arity et make_constructor de inductive_summary

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

1 files changed, 13 insertions, 2 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d235245e6..fda1190d1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -19,6 +19,7 @@ type mutual_inductive_packet = {
   mind_typename : identifier;
   mind_lc : constr;
   mind_arity : typed_type;
+  mind_nrealargs : int;
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool }
@@ -44,6 +45,7 @@ type mind_specif = {
 let mis_ntypes mis = mis.mis_mib.mind_ntypes
 let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
 let mis_nparams mis = mis.mis_mib.mind_nparams
+let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
 let mis_kelim mis = mis.mis_mip.mind_kelim
 let mis_recargs mis =
   Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
@@ -69,8 +71,6 @@ type inductive_summary = {
   nparams : int;
   nrealargs : int;
   nconstr : int;
-  make_arity : inductive -> constr list -> (name * constr) list * sorts;
-  make_constrs : inductive -> constr list -> constructor_summary array
 }
 
 let is_recursive listind = 
@@ -88,6 +88,17 @@ let mis_is_recursive mis =
 
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
 
+(* Annotation for cases *)
+let make_case_info mis style pats_source =
+  let constr_lengths = Array.map List.length (mis_recarg mis) in
+  let indsp = (mis.mis_sp,mis.mis_tyi) in
+  let print_info =
+    (indsp,mis_consnames mis,mis.mis_mip.mind_nrealargs,style,pats_source) in
+  (constr_lengths,print_info)
+
+let make_default_case_info mis =
+  make_case_info mis None (Array.init (mis_nconstr mis) (fun _ -> RegularPat))
+
 (*s Declaration. *)
 
 type mutual_inductive_entry = {