extension of the rename tactic: the following is now allowed:

 rename A into B, C into D, E into F.



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

5 files changed, 15 insertions, 10 deletions

diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 74ffc0a9c8..a8d2fb9500 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -752,7 +752,7 @@ let rec consider_match may_intro introduced available expected gls =
 		  consider_match may_intro ((id,false)::introduced) rest_ids rest
 	      | Name hid -> 
 		  tclTHENLIST 
-		    [rename_hyp id hid;
+		    [rename_hyp [id,hid];
 		     consider_match may_intro ((hid,true)::introduced) rest_ids rest]
 	  end
 	  begin
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b6c8f2ef89..55666a08a6 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -92,8 +92,8 @@ let h_clear b l = abstract_tactic (TacClear (b,l))
 let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l)
 let h_move dep id1 id2 =
   abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
-let h_rename id1 id2 =
-  abstract_tactic (TacRename (id1,id2)) (rename_hyp id1 id2)
+let h_rename l =
+  abstract_tactic (TacRename l) (rename_hyp l)
 
 (* Constructors *)
 let h_left l    = abstract_tactic (TacLeft l) (left_with_ebindings l)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 9c92ddcf2a..8937a37ef0 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -74,7 +74,7 @@ val h_lapply          : constr -> tactic
 val h_clear           : bool -> identifier list -> tactic
 val h_clear_body      : identifier list -> tactic
 val h_move            : bool -> identifier -> identifier -> tactic
-val h_rename          : identifier -> identifier -> tactic
+val h_rename          : (identifier*identifier) list -> tactic
 
 
 (* Constructors *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d52093230d..944b7710a5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -717,8 +717,11 @@ let rec intern_atomic lf ist x =
   | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
   | TacMove (dep,id1,id2) ->
     TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2)
-  | TacRename (id1,id2) -> TacRename (intern_hyp_or_metaid ist id1, intern_hyp_or_metaid ist id2)
-
+  | TacRename l -> 
+      TacRename (List.map (fun (id1,id2) -> 
+			     intern_hyp_or_metaid ist id1, 
+			     intern_hyp_or_metaid ist id2) l)
+	
   (* Constructors *)
   | TacLeft bl -> TacLeft (intern_bindings ist bl)
   | TacRight bl -> TacRight (intern_bindings ist bl)
@@ -2125,8 +2128,10 @@ and interp_atomic ist gl = function
   | TacClearBody l -> h_clear_body (interp_hyp_list ist gl l)
   | TacMove (dep,id1,id2) ->
       h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
-  | TacRename (id1,id2) ->
-      h_rename (interp_hyp ist gl id1) (interp_ident ist gl (snd id2))
+  | TacRename l ->
+      h_rename (List.map (fun (id1,id2) -> 
+			    interp_hyp ist gl id1, 
+			    interp_ident ist gl (snd id2)) l)
 
   (* Constructors *)
   | TacLeft bl -> h_left (interp_bindings ist gl bl)
@@ -2426,7 +2431,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacClear _ as x -> x
   | TacClearBody l as x -> x
   | TacMove (dep,id1,id2) as x -> x
-  | TacRename (id1,id2) as x -> x
+  | TacRename l as x -> x
 
   (* Constructors *)
   | TacLeft bl -> TacLeft (subst_bindings subst bl)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8de2498674..b0b76c4637 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -159,7 +159,7 @@ val keep          : identifier list -> tactic
 val new_hyp       : int option -> constr with_ebindings -> tactic
 
 val move_hyp      : bool -> identifier -> identifier -> tactic
-val rename_hyp    : identifier -> identifier -> tactic
+val rename_hyp    : (identifier * identifier) list -> tactic
 
 (*s Resolution tactics. *)