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

5 files changed, 26 insertions, 21 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2cca258b95..b8ba88185a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -517,7 +517,7 @@ let prim_refiner r sigma goal =
         let sg2 = mk_goal sign cl in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
-    | FixRule (f,n,rest) ->
+    | FixRule (f,n,rest,j) ->
      	let rec check_ind env k cl = 
           match kind_of_term (strip_outer_cast cl) with 
             | Prod (na,c1,b) -> 
@@ -531,7 +531,8 @@ let prim_refiner r sigma goal =
             | _ -> error "Not enough products."
 	in
 	let (sp,_) = check_ind env n cl in
-	let all = (f,n,cl)::rest in
+	let firsts,lasts = list_chop j rest in
+	let all = firsts@(f,n,cl)::lasts in
      	let rec mk_sign sign = function 
 	  | (f,n,ar)::oth ->
 	      let (sp',_)  = check_ind env n ar in 
@@ -539,14 +540,15 @@ let prim_refiner r sigma goal =
 		error ("Fixpoints should be on the same " ^ 
 		       "mutual inductive declaration.");
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error "Name already used in the environment";
+		error
+		  ("Name "^string_of_id f^" already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
 	in 
 	  (mk_sign sign all, sigma)
 	
-    | Cofix (f,others) ->
+    | Cofix (f,others,j) ->
      	let rec check_is_coind env cl = 
 	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
@@ -558,7 +560,8 @@ let prim_refiner r sigma goal =
 		  error ("All methods must construct elements " ^
 			  "in coinductive types.")
 	in
-	let all = (f,cl)::others in
+	let firsts,lasts = list_chop j others in
+	let all = firsts@(f,cl)::lasts in
      	List.iter (fun (_,c) -> check_is_coind env c) all;
         let rec mk_sign sign = function 
           | (f,ar)::oth ->
@@ -687,24 +690,26 @@ let prim_extractor subfun vl pft =
 	    mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
                     subfun (add_proof_var id vl) spf2)
 
-      | Some (Prim (FixRule (f,n,others)),spfl) ->
-	  let all = Array.of_list ((f,n,cl)::others) in
+      | Some (Prim (FixRule (f,n,others,j)),spfl) ->
+	  let firsts,lasts = list_chop j others in
+	  let all = Array.of_list (firsts@(f,n,cl)::lasts) in
 	  let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
 	  let names = Array.map (fun (f,_,_) -> Name f) all in
 	  let vn = Array.map (fun (_,n,_) -> n-1) all in
 	  let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
             (add_proof_var f vl) others in
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkFix ((vn,0),(names,lcty,lfix))	
+	    mkFix ((vn,j),(names,lcty,lfix))	
 
-      | Some (Prim (Cofix (f,others)),spfl) ->
-	  let all = Array.of_list ((f,cl)::others) in
+      | Some (Prim (Cofix (f,others,j)),spfl) ->
+	  let firsts,lasts = list_chop j others in
+	  let all = Array.of_list (firsts@(f,cl)::lasts) in
 	  let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
 	  let names  = Array.map (fun (f,_) -> Name f) all in
 	  let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
             (add_proof_var f vl) others in 
 	  let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
-	    mkCoFix (0,(names,lcty,lfix))
+	    mkCoFix (j,(names,lcty,lfix))
 	      
       | Some (Prim (Refine c),spfl) ->
 	  let mvl = collect_meta_variables c in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 9f81ffee7f..8a466d8df5 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -29,8 +29,8 @@ open Pattern
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
-  | FixRule of identifier * int * (identifier * int * constr) list
-  | Cofix of identifier * (identifier * constr) list
+  | FixRule of identifier * int * (identifier * int * constr) list * int
+  | Cofix of identifier * (identifier * constr) list * int
   | Refine of constr
   | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 5fb463da73..9db87d22e1 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -29,8 +29,8 @@ open Pattern
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
-  | FixRule of identifier * int * (identifier * int * constr) list
-  | Cofix of identifier * (identifier * constr) list
+  | FixRule of identifier * int * (identifier * int * constr) list * int
+  | Cofix of identifier * (identifier * constr) list * int
   | Refine of constr
   | Convert_concl of types * cast_kind 
   | Convert_hyp of named_declaration
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fa22de7bb2..40917b0854 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -214,11 +214,11 @@ let rec rename_hyp_no_check l gl = match l with
       tclTHEN (refiner (Prim (Rename (id1,id2)))) 
 	(rename_hyp_no_check l) gl
 
-let mutual_fix f n others gl = 
-  with_check (refiner (Prim (FixRule (f,n,others)))) gl
+let mutual_fix f n others j gl =
+  with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
 
-let mutual_cofix f others gl = 
-  with_check (refiner (Prim (Cofix (f,others)))) gl
+let mutual_cofix f others j gl =
+  with_check (refiner (Prim (Cofix (f,others,j)))) gl
     
 (* Versions with consistency checks *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 826337cc8d..581933c830 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -139,8 +139,8 @@ val move_hyp_no_check         :
 val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 val order_hyps : identifier list -> tactic
 val mutual_fix      :
-  identifier -> int -> (identifier * int * constr) list -> tactic
-val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+  identifier -> int -> (identifier * int * constr) list -> int -> tactic
+val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
 
 (*s The most primitive tactics with consistency and type checking *)