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

12 files changed, 52 insertions, 44 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 267d550a9..37083eb46 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -427,10 +427,11 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++ 
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 	
-  | FixRule (f,n,[]) ->
+  | FixRule (f,n,[],_) ->
       (str"fix " ++ pr_id f ++ str"/" ++ int n)
       
-  | FixRule (f,n,others) -> 
+  | FixRule (f,n,others,j) -> 
+      if j<>0 then warning "Unsupported printing of \"fix\"";
       let rec print_mut = function
 	| (f,n,ar)::oth -> 
            pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -438,10 +439,11 @@ let pr_prim_rule = function
       (str"fix " ++ pr_id f ++ str"/" ++ int n ++
          str" with " ++ print_mut others)
 
-  | Cofix (f,[]) ->
+  | Cofix (f,[],_) ->
       (str"cofix " ++ pr_id f)
 
-  | Cofix (f,others) ->
+  | Cofix (f,others,j) ->
+      if j<>0 then warning "Unsupported printing of \"fix\"";
       let rec print_mut = function
 	| (f,ar)::oth ->
 	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 378f9972e..445b193f8 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -58,8 +58,8 @@ let explore_tree pfs =
     | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
     | Intro identifier -> "Intro"
     | Cut (bool, _, identifier, types) -> "Cut"
-    | FixRule (identifier, int, l) -> "FixRule"
-    | Cofix (identifier, l) -> "Cofix"
+    | FixRule (identifier, int, l, _) -> "FixRule"
+    | Cofix (identifier, l, _) -> "Cofix"
     | Convert_concl (types, cast_kind) -> "Convert_concl"
     | Convert_hyp named_declaration -> "Convert_hyp"
     | Thin identifier_list -> "Thin"
@@ -411,8 +411,8 @@ and depends_of_prim_rule pr acc = match pr with
   | Refine c                     -> depends_of_constr c acc
   | Intro id                     -> acc
   | Cut (_, _, _, t)             -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
-  | FixRule (_, _, l)            -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
-  | Cofix (_, l)                 -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+  | FixRule (_, _, l, _)         -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+  | Cofix (_, l, _)              -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
   | Convert_concl (t, _)         -> depends_of_constr t acc
   | Convert_hyp (_, None, t)     -> depends_of_constr t acc
   | Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index a501fb6a6..7503d6328 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -82,8 +82,8 @@ let first_word s =
 let string_of_prim_rule x = match x with
   | Proof_type.Intro _-> "Intro"
   | Proof_type.Cut _ -> "Cut"
-  | Proof_type.FixRule (_,_,_) -> "FixRule"
-  | Proof_type.Cofix (_,_)-> "Cofix"
+  | Proof_type.FixRule _ -> "FixRule"
+  | Proof_type.Cofix _ -> "Cofix"
   | Proof_type.Refine _ -> "Refine"
   | Proof_type.Convert_concl _ -> "Convert_concl"
   | Proof_type.Convert_hyp _->"Convert_hyp"
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2cca258b9..b8ba88185 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 9f81ffee7..8a466d8df 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 5fb463da7..9db87d22e 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 fa22de7bb..40917b085 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 826337cc8..581933c83 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 *)
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 2aff94b64..4b89cbcb4 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 46c8d3aa2..f1ecc4da9 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 3d3b22045..c3c1c4505 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 dd18aa86a..e00088dd8 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. *)