Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0

instead of the index required by the user; extended FixRule and
Cofix accordingly).

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

4 files changed, 14 insertions, 13 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 2aff94b640..4b89cbcb4f 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -55,13 +55,13 @@ let h_fix ido n      = abstract_tactic (TacFix (ido,n)) (fix ido n)
 let h_mutual_fix b id n l =
   abstract_tactic
     (TacMutualFix (b,id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
-    (mutual_fix id n l)
+    (mutual_fix id n l 0)
 
 let h_cofix ido      = abstract_tactic (TacCofix ido) (cofix ido)
 let h_mutual_cofix b id l =
   abstract_tactic
     (TacMutualCofix (b,id,List.map (fun (id,c) -> (id,inj_open c)) l)) 
-    (mutual_cofix id l)
+    (mutual_cofix id l 0)
 
 let h_cut c          = abstract_tactic (TacCut (inj_open c)) (cut c)
 let h_generalize_gen cl =
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 46c8d3aa2e..f1ecc4da91 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -330,29 +330,30 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
           gl
 
     (* fix => tactique Fix *)
-    | Fix ((ni,_),(fi,ai,_)) , _ ->
+    | Fix ((ni,j),(fi,ai,_)) , _ ->
 	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
+	let firsts,lasts = list_chop j (Array.to_list fixes) in
 	tclTHENS
-	  (mutual_fix (out_name fi.(0)) (succ ni.(0))
-	    (List.tl (Array.to_list fixes)))
+	  (mutual_fix (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux subst th) sgp)
 	  gl
 
     (* cofix => tactique CoFix *)
-    | CoFix (_,(fi,ai,_)) , _ ->
+    | CoFix (j,(fi,ai,_)) , _ ->
 	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
+	let firsts,lasts = list_chop j (Array.to_list cofixes) in
 	tclTHENS
-	  (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes)))
+	  (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
 		       | None -> tclIDTAC 
 		       | Some th -> tcc_aux subst th) sgp)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3d3b220457..c3c1c45054 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -174,18 +174,18 @@ let mutual_fix = Tacmach.mutual_fix
 
 let fix ido n gl = match ido with
   | None -> 
-      mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] gl
+      mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] 0 gl
   | Some id ->
-      mutual_fix id n [] gl
+      mutual_fix id n [] 0 gl
 
 (* Refine as a cofixpoint *)
 let mutual_cofix = Tacmach.mutual_cofix
 
 let cofix ido gl = match ido with
   | None -> 
-      mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] gl
+      mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] 0 gl
   | Some id ->
-      mutual_cofix id [] gl
+      mutual_cofix id [] 0 gl
 
 (**************************************************************)
 (*          Reduction and conversion tactics                  *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index dd18aa86ac..e00088dd8a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -53,9 +53,9 @@ val convert_concl   : constr -> cast_kind -> tactic
 val convert_hyp     : named_declaration -> tactic
 val thin            : identifier list -> tactic
 val mutual_fix      :
-  identifier -> int -> (identifier * int * constr) list -> tactic
+  identifier -> int -> (identifier * int * constr) list -> int -> tactic
 val fix             : identifier option -> int -> tactic
-val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
 val cofix           : identifier option -> tactic
 
 (*s Introduction tactics. *)