- Reforme de la gestion des args recursifs (via arbres reguliers)

- coqtop -byte -opt bouclait!


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

3 files changed, 11 insertions, 15 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index e6def959b5..0c08da467b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -64,7 +64,7 @@ let match_with_conjunction t =
     | Ind ind -> 
 	let (mib,mip) = Global.lookup_inductive ind in
 	if (Array.length mip.mind_consnames = 1)
-	  && (not (mis_is_recursive (mib,mip)))
+	  && (not (mis_is_recursive (ind,mib,mip)))
           && (mip.mind_nrealargs = 0)
         then 
 	  Some (hdapp,args)
@@ -81,12 +81,10 @@ let match_with_disjunction t =
   let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
     | Ind ind  ->
-	let (mib,mip) = Global.lookup_inductive ind in
-        let constr_types = mip.mind_nf_lc in
-        let only_one_arg c =
-	  ((nb_prod c) - mip.mind_nparams) = 1 in 
-	if (array_for_all only_one_arg constr_types) &&
-          (not (mis_is_recursive (mib,mip)))
+        let car = mis_constr_nargs ind in
+	if array_for_all (fun ar -> ar = 1) car &&
+	   (let (mib,mip) = Global.lookup_inductive ind in
+            not (mis_is_recursive (ind,mib,mip)))
         then 
 	  Some (hdapp,args)
         else 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d7b1eddbc3..70716cde2d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -259,8 +259,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
   let rec analrec c recargs =
     match kind_of_term c, recargs with 
     | Prod (_,_,c), recarg::rest ->
-	  (match recarg with
-	    | Param _ -> false :: (analrec c rest)
+	  (match dest_recarg recarg with
 	    | Norec   -> false :: (analrec c rest)
 	    | Imbr _  -> false :: (analrec c rest)
 	    | Mrec j  -> (isrec & j=k) :: (analrec c rest))
@@ -272,7 +271,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
   let n = mip.mind_nparams in
   let lc =
     Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
-  let lrecargs = mip.mind_listrec in
+  let lrecargs = dest_subterms mip.mind_recargs in
   array_map2 analrec lc lrecargs
 
 let case_sign = compute_construtor_signatures false
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 72bf8a076b..b338e1c702 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1438,19 +1438,18 @@ let is_indhyp p n t =
 (* eliminator _ind, _rec or _rect, or eliminator built by Scheme) *)
 let compute_elim_signature_and_roughly_check elimt mind =
   let (mib,mip) = Global.lookup_inductive mind in
-  let lra = mip.mind_listrec in
+  let lra = dest_subterms mip.mind_recargs in
   let nconstr = Array.length mip.mind_consnames in
   let _,elimt2 = decompose_prod_n mip.mind_nparams elimt in
   let n = nb_prod elimt2 in
   let npred = n - nconstr - mip.mind_nrealargs - 1 in
   let rec check_branch p c ra = match kind_of_term c, ra with
-    | Prod (_,_,c), Declarations.Mrec i :: ra' ->
-	(match kind_of_term c with
-	   | Prod (_,t,c) when is_indhyp (p+1) npred t ->
+    | Prod (_,_,c), r :: ra' ->
+	(match dest_recarg r, kind_of_term c with
+	   | Mrec i, Prod (_,t,c) when is_indhyp (p+1) npred t ->
 	       true::(check_branch (p+2) c ra')
 	   | _ -> false::(check_branch (p+1) c ra'))
     | LetIn (_,_,_,c), ra' -> false::(check_branch (p+1) c ra)
-    | Prod (_,_,c), _ :: ra -> false::(check_branch (p+1) c ra)
     | _, [] -> []
     | _ ->
 	error"Not a recursive eliminator: some constructor argument is lacking"