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

5 files changed, 41 insertions, 43 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e0dec159b0..e1c4caad77 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -358,7 +358,7 @@ let _ =
 	   begin 
 	     try
 	       let trad = Declare.global_reference CCI in
-	       let rectype = trad c in
+	       let rectype = destMutInd (trad c) in
 	       let consnames = 
 		 mis_consnames (Global.lookup_mind_specif rectype) in
 	       let lcons = 
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index dcc3a5f7b1..fc5b6a4466 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -219,8 +219,8 @@ let match_with_non_recursive_type t =
     | IsAppL _ -> 
         let (hdapp,args) = decomp_app t in
         (match kind_of_term hdapp with
-           | IsMutInd _ -> 
-               if not (Global.mind_is_recursive hdapp) then 
+           | IsMutInd ind -> 
+               if not (Global.mind_is_recursive ind) then 
 		 Some (hdapp,args) 
 	       else 
 		 None 
@@ -235,11 +235,11 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
 let match_with_conjunction t =
   let (hdapp,args) = decomp_app t in 
   match kind_of_term hdapp with
-    | IsMutInd _ -> 
-        let nconstr = Global.mind_nconstr hdapp in  
+    | IsMutInd ind -> 
+        let nconstr = Global.mind_nconstr ind in  
 	if (nconstr = 1) && 
-          (not (Global.mind_is_recursive hdapp)) &&
-          (nb_prod (Global.mind_arity hdapp)) = (Global.mind_nparams hdapp)
+          (not (Global.mind_is_recursive ind)) &&
+          (nb_prod (Global.mind_arity ind)) = (Global.mind_nparams ind)
         then 
 	  Some (hdapp,args)
         else 
@@ -254,13 +254,13 @@ let is_conjunction t = op2bool (match_with_conjunction t)
 let match_with_disjunction t =
   let (hdapp,args) = decomp_app t in 
   match kind_of_term hdapp with
-    | IsMutInd _  -> 
+    | IsMutInd ind  ->
         let constr_types = 
-	  Global.mind_lc_without_abstractions hdapp in
+	  Global.mind_lc_without_abstractions ind in
         let only_one_arg c = 
-	  ((nb_prod c) - (Global.mind_nparams hdapp)) = 1 in 
+	  ((nb_prod c) - (Global.mind_nparams ind)) = 1 in 
 	if (array_for_all only_one_arg constr_types) &&
-          (not (Global.mind_is_recursive hdapp))
+          (not (Global.mind_is_recursive ind))
         then 
 	  Some (hdapp,args)
         else 
@@ -272,8 +272,8 @@ let is_disjunction t = op2bool (match_with_disjunction t)
 let match_with_empty_type t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
-    | IsMutInd _ -> 
-        let nconstr = Global.mind_nconstr hdapp in  
+    | IsMutInd ind -> 
+        let nconstr = Global.mind_nconstr ind in  
 	if nconstr = 0 then Some hdapp else None
     | _ ->  None
 	  
@@ -282,11 +282,11 @@ let is_empty_type t = op2bool (match_with_empty_type t)
 let match_with_unit_type t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
-    | IsMutInd _  -> 
+    | IsMutInd ind  -> 
         let constr_types = 
-	  Global.mind_lc_without_abstractions hdapp in 
-        let nconstr = Global.mind_nconstr hdapp in
-        let zero_args c = ((nb_prod c) - (Global.mind_nparams hdapp)) = 0 in  
+	  Global.mind_lc_without_abstractions ind in 
+        let nconstr = Global.mind_nconstr ind in
+        let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in  
 	if nconstr = 1 && (array_for_all zero_args constr_types) then 
 	  Some hdapp
         else 
@@ -303,12 +303,12 @@ let is_unit_type t = op2bool (match_with_unit_type t)
 let match_with_equation  t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
-    | IsMutInd _  -> 
+    | IsMutInd ind -> 
         let constr_types = 
-	  Global.mind_lc_without_abstractions hdapp in 
+	  Global.mind_lc_without_abstractions ind in 
         let refl_rel_term1 = put_pat mmk "(A:?)(x:A)(? A x x)" in
         let refl_rel_term2 = put_pat mmk "(x:?)(? x x)" in
-        let nconstr = Global.mind_nconstr hdapp in
+        let nconstr = Global.mind_nconstr ind in
 	if nconstr = 1 &&
            (somatches constr_types.(0) refl_rel_term1 ||
             somatches constr_types.(0) refl_rel_term2) 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 4755cc50ea..891f411a18 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -229,7 +229,7 @@ let ifOnClause pred tac1 tac2 cls gl =
   the elimination. *)
 
 type branch_args = {
-  ity        : constr;      (* the type we were eliminating on *)
+  ity        : inductive;   (* the type we were eliminating on *)
   largs      : constr list; (* its arguments *)
   branchnum  : int;         (* the branch number *)
   pred       : constr;      (* the predicate we used *)
@@ -245,16 +245,15 @@ type branch_assumptions = {
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
   indargs   : identifier list} (* the inductive arguments *)
 
-
 (* Hum ... the following function looks quite similar to the one 
- * defined with the same name in Tactics.ml. 
+ * (previously) defined with the same name in Tactics.ml. 
  *  --Eduardo (11/8/97) *)
 
-let reduce_to_ind gl t = 
+let reduce_to_ind_goal gl t = 
   let rec elimrec t l = 
     match decomp_app(t) with
-      | (DOPN(MutInd (sp,_),_) as mind,_) -> 
-	  (mind,mind_path mind,t,prod_it t l)
+      | (DOPN(MutInd ind_sp,args) as mind,_) -> 
+	  ((ind_sp,args),path_of_inductive_path ind_sp,t,prod_it t l)
       | (DOPN(Const _,_),_) -> 
 	  elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t)) l
       | (DOP2(Cast,c,_),[]) -> elimrec c l
@@ -272,7 +271,7 @@ let case_sign ity i =
   analrec [] recarg.(i-1)
 
 let elim_sign ity i =
-  let (_,j,_) = destMutInd ity in
+  let (_,j),_ = ity in
   let rec analrec acc = function 
     | (Param(_)::rest) -> analrec (false::acc) rest
     | (Norec::rest)    -> analrec (false::acc) rest
@@ -313,7 +312,7 @@ let last_arg = function
 
 let general_elim_then_using 
   elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl =
-  let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let name_elim =
     (match elim with
        | DOPN(Const sp,_) -> id_of_string(string_of_path sp)
@@ -361,7 +360,7 @@ let general_elim_then_using
 
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
-  let (ity,path_name,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let (ity,path_name,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let elim = 
     lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl))
   in
@@ -374,7 +373,7 @@ let simple_elimination_then tac = elimination_then tac ([],[])
 
 let case_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
-  let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
   let elim  = Indrec.make_case_gen (pf_env gl) sigma ity sort in  
@@ -383,7 +382,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl =
 
 let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
-  let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
+  let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
   let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
@@ -448,3 +447,4 @@ let make_case_branch_assumptions ba gl =
      with Failure _ -> anomaly "make_case_branch_assumptions")
 
 let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
+
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4ac1fb41d0..7884ba02eb 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -83,7 +83,7 @@ val conclPattern : constr -> constr -> Coqast.t -> tactic
 (*s Elimination tacticals. *)
 
 type branch_args = { 
-  ity        : constr;      (* the type we were eliminating on *)
+  ity        : inductive;   (* the type we were eliminating on *)
   largs      : constr list; (* its arguments *)
   branchnum  : int;         (* the branch number *)
   pred       : constr;      (* the predicate we used *)
@@ -105,7 +105,7 @@ val lookup_eliminator :
   typed_type signature -> section_path -> string -> constr
 
 val general_elim_then_using :
-  constr ->  (constr -> int -> bool list) -> 
+  constr ->  (inductive -> int -> bool list) -> 
     (branch_args -> tactic) -> constr option -> 
       (arg_bindings * arg_bindings) -> constr -> tactic
 	  
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8759e54a9a..4791209298 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -48,8 +48,8 @@ let get_commands =
 let rec string_head_bound = function 
   | DOPN(Const _,_) as x -> 
       string_of_id (basename (path_of_const x))
-  | DOPN(MutInd _,_) as x -> 
-      let mispec = Global.lookup_mind_specif x in 
+  | DOPN(MutInd ind_sp,args) as x -> 
+      let mispec = Global.lookup_mind_specif (ind_sp,args) in 
       string_of_id (mis_typename mispec)
   |  DOPN(MutConstruct ((sp,tyi),i),_) ->
        let mib = Global.lookup_mind sp in
@@ -833,7 +833,6 @@ let dyn_move_dep = function
 let constructor_checking_bound  boundopt i lbind gl =
   let cl = pf_concl gl in 
   let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in 
-  let (x_0,x_1,args) = destMutInd mind in
   let nconstr = mis_nconstr (Global.lookup_mind_specif mind) 
   and sigma   = project gl in
   if i=0 then error "The constructors are numbered starting from 1";
@@ -844,7 +843,7 @@ let constructor_checking_bound  boundopt i lbind gl =
 	  error "Not the expected number of constructors"
     | None -> ()
   end;
-  let cons = DOPN(MutConstruct((x_0,x_1),i),args) in
+  let cons = mkMutConstruct (ith_constructor_of_inductive mind i) in
   let apply_tac = apply_with_bindings (cons,lbind) in
   (tclTHENLIST [convert_concl redcl; intros; apply_tac]) gl
 
@@ -853,7 +852,6 @@ let one_constructor i = (constructor_checking_bound None i)
 let any_constructor gl = 
   let cl = pf_concl gl in 
   let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in
-  let (x_0,x_1,args) = destMutInd mind in
   let nconstr = mis_nconstr (Global.lookup_mind_specif mind)
   and sigma   = project gl in
   if nconstr = 0 then error "The type has no constructors";
@@ -1003,9 +1001,9 @@ let simplest_elim c = default_elim (c,[])
 
 
 let rec is_rec_arg indpath t =
-  try 
-    Declare.mind_path (fst (find_mrectype (Global.env()) Evd.empty t)) 
-    = indpath
+  try
+    let ((ind_sp,_),_) = find_mrectype (Global.env()) Evd.empty t in
+    Declare.path_of_inductive_path ind_sp = indpath
   with Induc -> 
     false
 
@@ -1265,9 +1263,9 @@ let induction_from_context hyp0 gl =
   let sign = pf_untyped_hyps gl in
   let tsign = pf_hyps gl in
   let tmptyp0 = pf_get_hyp gl hyp0 in
-  let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in
+  let ((ind_sp,_) as mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in
   let indvars = find_atomic_param_of_ind mind indtyp in
-  let mindpath = Declare.mind_path mind in
+  let mindpath = Declare.path_of_inductive_path ind_sp in
   let elimc = lookup_eliminator tsign mindpath (suff gl (pf_concl gl)) in
   let elimt = pf_type_of gl elimc in
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars sign in