Nouveaux types 'constructor' et 'inductive' dans Term;

les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.


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

3 files changed, 38 insertions, 32 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index fcda9fb93e..3920786110 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -38,15 +38,15 @@ let pr_qualified sp id =
   else 
     [< 'sTR(string_of_path sp) >]
 
-let pr_constant sp = pr_qualified sp (basename sp)
+let pr_constant (sp,_) = pr_qualified sp (basename sp)
 
-let pr_existential ev = [< 'sTR ("?" ^ string_of_int ev) >]
+let pr_existential (ev,_) = [< 'sTR ("?" ^ string_of_int ev) >]
 
-let pr_inductive (sp,tyi as ind_sp) =
+let pr_inductive (sp,tyi as ind_sp,_) =
   let id = id_of_global (MutInd ind_sp) in
   pr_qualified sp id
 
-let pr_constructor ((sp,tyi),i as cstr_sp) =
+let pr_constructor ((sp,tyi),i as cstr_sp,_) =
   let id = id_of_global (MutConstruct cstr_sp) in
   pr_qualified sp id
 
@@ -62,16 +62,16 @@ let globpr k gt = match gt with
   | Nvar(_,s) -> [< 'sTR s >]
   | Node(_,"EVAR", (Num (_,ev))::_) ->
       if !print_arguments then dfltpr gt
-      else pr_existential ev
+      else pr_existential (ev,[])
   | Node(_,"CONST",(Path(_,sl,s))::_) ->
       if !print_arguments then dfltpr gt
-      else pr_constant (section_path sl s)
+      else pr_constant (section_path sl s,[])
   | Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) ->
       if !print_arguments then (dfltpr gt)
-      else pr_inductive (section_path sl s,tyi)
+      else pr_inductive ((section_path sl s,tyi),[])
   | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) ->
       if !print_arguments then (dfltpr gt)
-      else pr_constructor ((section_path sl s,tyi),i)
+      else pr_constructor (((section_path sl s,tyi),i),[])
   | gt -> dfltpr gt
 
 let apply_prec = Some (("Term",(9,0,0)),Extend.L)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 217ec6197d..0f704c552b 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -27,10 +27,10 @@ val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
 val prrawterm       : Rawterm.rawconstr -> std_ppcmds
 val prpattern       : Rawterm.pattern -> std_ppcmds
 
-val pr_constant     : section_path -> std_ppcmds
-val pr_existential  : existential_key -> std_ppcmds
-val pr_constructor  : constructor_path -> std_ppcmds
-val pr_inductive    : inductive_path -> std_ppcmds
+val pr_constant     : constant -> std_ppcmds
+val pr_existential  : existential -> std_ppcmds
+val pr_constructor  : constructor -> std_ppcmds
+val pr_inductive    : inductive -> std_ppcmds
 
 val pr_sign         : var_context -> std_ppcmds
 val pr_env_opt      : context -> std_ppcmds
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 1e6ff11fc8..b33ea00534 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -96,10 +96,12 @@ let occur_id env id0 c =
     | VAR id             -> id=id0
     | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
     | DOPN (Abst sp,cl)  -> (basename sp = id0) or (array_exists (occur n) cl)
-    | DOPN (MutInd _, cl) as t -> 
-  	(basename (mind_path t) = id0) or (array_exists (occur n) cl)
-    | DOPN (MutConstruct _, cl) as t -> 
-    	(basename (mind_path t) = id0) or (array_exists (occur n) cl)
+    | DOPN (MutInd ind_sp, cl) as t -> 
+  	(basename (path_of_inductive_path ind_sp) = id0)
+	or (array_exists (occur n) cl)
+    | DOPN (MutConstruct cstr_sp, cl) as t -> 
+    	(basename (path_of_constructor_path cstr_sp) = id0)
+	or (array_exists (occur n) cl)
     | DOPN(_,cl)         -> array_exists (occur n) cl
     | DOP1(_,c)          -> occur n c
     | DOP2(_,c1,c2)      -> (occur n c1) or (occur n c2)
@@ -137,10 +139,12 @@ let global_vars_and_consts t =
     | VAR id             -> id::acc
     | DOPN (Const sp,cl) -> (basename sp)::(Array.fold_left collect acc cl)
     | DOPN (Abst sp,cl)  -> (basename sp)::(Array.fold_left collect acc cl)
-    | DOPN (MutInd _, cl) as t       -> 
-	(basename (mind_path t))::(Array.fold_left collect acc cl)
-    | DOPN (MutConstruct _, cl) as t -> 
-	(basename (mind_path t))::(Array.fold_left collect acc cl)
+    | DOPN (MutInd ind_sp, cl) as t       -> 
+	(basename (path_of_inductive_path ind_sp))
+	::(Array.fold_left collect acc cl)
+    | DOPN (MutConstruct cstr_sp, cl) as t -> 
+	(basename (path_of_constructor_path cstr_sp))
+	::(Array.fold_left collect acc cl)
     | DOPN(_,cl)         -> Array.fold_left collect acc cl
     | DOP1(_,c)          -> collect acc c
     | DOP2(_,c1,c2)      -> collect (collect acc c1) c2
@@ -485,23 +489,24 @@ let old_bdize_depcast opcast at_top env t =
 	   | IsAbst (sp,cl) ->
 	       ope("ABST",((path_section dummy_loc sp)::
 			   (array_map_to_list (bdrec avoid env) cl)))
-	   | IsMutInd (sp,tyi,cl) ->
+	   | IsMutInd ((sp,tyi),cl) ->
 	       ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
 			     (array_map_to_list (bdrec avoid env) cl)))
-	   | IsMutConstruct (sp,tyi,n,cl) ->
+	   | IsMutConstruct (((sp,tyi),n),cl) ->
 	       ope("MUTCONSTRUCT",
 		   ((path_section dummy_loc sp)::(num tyi)::(num n)::
 		    (array_map_to_list (bdrec avoid env) cl)))
 	   | IsMutCase (annot,p,c,bl) ->
 	       let synth_type = synthetize_type () in
 	       let tomatch = bdrec avoid env c in
-	       begin match annot with
-		 | None -> 
+	       begin 
+		 match annot with
+(*		 | None -> 
 	             (* Pas d'annotation --> affichage avec vieux Case *)
 		     let pred = bdrec avoid env p in
 		     let bl' = array_map_to_list (bdrec avoid env) bl in
 		     ope("MUTCASE",pred::tomatch::bl')
-		 | Some indsp ->
+		 | Some *) indsp ->
 		     let (mib,mip as lmis) = 
 		       mind_specif_of_mind_light indsp in
 		     let lc = lc_of_lmis lmis in
@@ -714,21 +719,22 @@ let rec detype avoid env t =
 	RRef(dummy_loc,REVar(ev,ids_of_var (Array.map (detype avoid env) cl)))
     | IsAbst (sp,cl) -> 
 	anomaly "bdize: Abst should no longer occur in constr"
-    | IsMutInd (sp,tyi,cl) ->
+    | IsMutInd (ind_sp,cl) ->
 	let ids = ids_of_var (Array.map (detype avoid env) cl) in
-	RRef (dummy_loc,RInd ((sp,tyi),ids))
-    | IsMutConstruct (sp,tyi,n,cl) ->
+	RRef (dummy_loc,RInd (ind_sp,ids))
+    | IsMutConstruct (cstr_sp,cl) ->
 	let ids = ids_of_var (Array.map (detype avoid env) cl) in
-	RRef (dummy_loc,RConstruct (((sp,tyi),n),ids))
+	RRef (dummy_loc,RConstruct (cstr_sp,ids))
     | IsMutCase (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
 	let tomatch = detype avoid env c in
-	begin match annot with
-	  | None -> (* Pas d'annotation --> affichage avec vieux Case *)
+	begin 
+	  match annot with
+(*	  | None -> (* Pas d'annotation --> affichage avec vieux Case *)
 	      warning "Printing in old Case syntax";
 	      ROldCase (dummy_loc,false,Some (detype avoid env p),
 			tomatch,Array.map (detype avoid env) bl)
-	  | Some indsp ->
+	  | Some *) indsp ->
 	      let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
 	      let lc = lc_of_lmis lmis in
 	      let lcparams = Array.map get_params lc in