Effets de bords suite à la restructuration des inductives (cf Inductive)

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

3 files changed, 13 insertions, 12 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 703bfb7786..d31a71845b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -7,6 +7,7 @@ open Names
 open Generic
 open Term
 open Reduction
+open Inductive
 open Evd
 open Environ
 open Proof_trees
@@ -133,10 +134,9 @@ let match_with_conjunction t =
   let (hdapp,args) = decomp_app t in 
   match kind_of_term hdapp with
     | IsMutInd ind -> 
-        let nconstr = Global.mind_nconstr ind in  
-	if (nconstr = 1) && 
-          (not (Global.mind_is_recursive ind)) &&
-          (nb_prod (Global.mind_arity ind)) = (Global.mind_nparams ind)
+	let mispec = Global.lookup_mind_specif ind in
+	if (mis_nconstr mispec = 1)
+	  && (not (mis_is_recursive mispec)) && (mis_nrealargs mispec = 0)
         then 
 	  Some (hdapp,args)
         else 
@@ -152,12 +152,12 @@ let match_with_disjunction t =
   let (hdapp,args) = decomp_app t in 
   match kind_of_term hdapp with
     | IsMutInd ind  ->
-        let constr_types = 
-	  Global.mind_lc_without_abstractions ind in
-        let only_one_arg c = 
-	  ((nb_prod c) - (Global.mind_nparams ind)) = 1 in 
+	let mispec = Global.lookup_mind_specif ind in
+        let constr_types = mis_lc_without_abstractions mispec in
+        let only_one_arg c =
+	  ((nb_prod c) - (mis_nparams mispec)) = 1 in 
 	if (array_for_all only_one_arg constr_types) &&
-          (not (Global.mind_is_recursive ind))
+          (not (mis_is_recursive mispec))
         then 
 	  Some (hdapp,args)
         else 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c8f6876988..6f8d55ef6f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -7,6 +7,7 @@ open Names
 open Generic
 open Term
 open Sign
+open Constant
 open Inductive
 open Reduction
 open Environ
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c35109e2c3..8803933e94 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -54,9 +54,9 @@ let rec string_head_bound = function
   | 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
-       string_of_id (mib.mind_packets.(tyi).mind_consnames.(i-1))
+  |  DOPN(MutConstruct (ind_sp,i),args) ->
+       let mispec = Global.lookup_mind_specif (ind_sp,args) in 
+       string_of_id (mis_consnames mispec).(i-1)
   |  VAR id -> string_of_id id
   |  _ -> raise Bound