Simplification de Proof_type.prim_rule

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

3 files changed, 26 insertions, 29 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index 7567ae35eb..ddddd21d88 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -296,16 +296,14 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 
     (* fix => tactique Fix *)
     | Fix ((ni,_),(fi,ai,_)) , _ ->
-	let ids =
-	  Array.to_list
-            (Array.map
-              (function Name id -> id
-                | _ -> error "recursive functions must have names !")
-              fi) 
+	let out_name = function
+	  | Name id -> id
+          | _ -> error "recursive functions must have names !"
 	in
+	let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
 	tclTHENS
-	  (mutual_fix ids (List.map succ (Array.to_list ni))
-             (List.tl (Array.to_list ai)))
+	  (mutual_fix (out_name fi.(0)) (succ ni.(0))
+	    (List.tl (Array.to_list fixes)))
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux th) sgp)
@@ -313,15 +311,13 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 
     (* cofix => tactique CoFix *)
     | CoFix (_,(fi,ai,_)) , _ ->
-	let ids =
-	  Array.to_list
-            (Array.map
-              (function Name id -> id
-                | _ -> error "recursive functions must have names !")
-              fi) 
+	let out_name = function
+	  | Name id -> id
+          | _ -> error "recursive functions must have names !"
 	in
+	let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
 	tclTHENS
-	  (mutual_cofix ids (List.tl (Array.to_list ai)))
+	  (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes)))
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux th) sgp)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f8b6282703..ef9222a309 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -105,7 +105,7 @@ let move_hyp        = Tacmach.move_hyp
 let rename_hyp      = Tacmach.rename_hyp
 
 let mutual_fix   = Tacmach.mutual_fix
-let fix f n      = mutual_fix [f] [n] []
+let fix f n      = mutual_fix f n []
 
 let fix_noname n =  
   let id = Pfedit.get_current_proof_name () in
@@ -116,18 +116,18 @@ let dyn_mutual_fix argsl gl =
     | [Integer n]                          -> fix_noname n gl
     | [Identifier id;Integer n]            -> fix id n gl
     | ((Identifier id)::(Integer n)::lfix) -> 
-	let rec decomp lid ln lar = function
+	let rec decomp lar = function
           | (Fixexp (id,n,ar)::rest) -> 
-	      decomp (id::lid) (n::ln) (ar::lar) rest
-          | [] -> (List.rev lid,List.rev ln,List.rev lar)
+	      decomp ((id,n,pf_interp_constr gl ar)::lar) rest
+          | [] -> (List.rev lar)
 	  | _  -> bad_tactic_args "mutual_fix" argsl
 	in
-	let (lid,ln,lar) = decomp [] [] [] lfix in
-	mutual_fix (id::lid) (n::ln) (List.map (pf_interp_constr gl) lar) gl
+	let lar = decomp [] lfix in
+	mutual_fix id n lar gl
     | l -> bad_tactic_args "mutual_fix" l 
 
 let mutual_cofix = Tacmach.mutual_cofix
-let cofix f      =  mutual_cofix [f] []
+let cofix f      =  mutual_cofix f []
 
 let cofix_noname n =  
   let id = Pfedit.get_current_proof_name () in
@@ -138,14 +138,14 @@ let dyn_mutual_cofix argsl gl =
     | []                       -> cofix_noname gl
     | [(Identifier id)]        -> cofix id gl
     | ((Identifier id)::lcofix) -> 
-	let rec decomp lid lar = function 
+	let rec decomp lar = function 
           | (Cofixexp (id,ar)::rest) -> 
-              decomp (id::lid) (ar::lar) rest
-          | [] -> (List.rev lid,List.rev lar)
+              decomp ((id,pf_interp_constr gl ar)::lar) rest
+          | [] -> List.rev lar
 	  |  _ -> bad_tactic_args "mutual_cofix" argsl
 	in
-	let (lid,lar) = decomp [] [] lcofix in
-        mutual_cofix (id::lid) (List.map (pf_interp_constr gl) lar) gl
+	let lar = decomp [] lcofix in
+        mutual_cofix id lar gl
    | l -> bad_tactic_args "mutual_cofix" l 
 
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 19cd032b0c..a1c961400d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -45,9 +45,10 @@ val refine          : constr -> tactic
 val convert_concl   : constr -> tactic
 val convert_hyp     : named_declaration -> tactic
 val thin            : identifier list -> tactic
-val mutual_fix      : identifier list -> int list -> constr list -> tactic
+val mutual_fix      :
+  identifier -> int -> (identifier * int * constr) list -> tactic
 val fix             : identifier -> int -> tactic
-val mutual_cofix    : identifier list -> constr list -> tactic
+val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
 val cofix           : identifier -> tactic
 
 val dyn_mutual_fix   : tactic_arg list -> tactic