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

12 files changed, 46 insertions, 23 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index be50c4bdbe..ba17a23eea 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -140,7 +140,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
       [tclTHENLIST 
       [	
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
-	(* observe_tac "change_hyp_with_using rename " *) (h_rename prov_id hyp_id)
+	(* observe_tac "change_hyp_with_using rename " *) (h_rename [prov_id,hyp_id])
       ]] g
 
 exception TOREMOVE
@@ -573,7 +573,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	  tclTHENLIST[
 	    forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
 	    thin [hid];
-	    h_rename prov_hid hid
+	    h_rename [prov_hid,hid]
 	  ] g
       )
       ( (*
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d04d8e3134..0ba9553ce4 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -204,6 +204,15 @@ This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current
 context\footnote{but it does not rename the hypothesis in the
   proof-term...}
 
+\begin{Variants}
+
+\item {\tt rename {\ident$_1$} into {\ident$_2$}, \ldots,
+    {\ident$_{2k-1}$} into {\ident$_{2k}$}}
+
+ Is equivalent to the sequence of the corresponding atomic {\tt rename}. 
+
+\end{Variants}
+
 \begin{ErrMsgs}
 
 \item \errindex{{\ident$_2$} not found}
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9f783771b7..3853a6d51c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -314,6 +314,9 @@ GEXTEND Gram
     [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
       | -> TacId [] ] ]
   ;
+  rename : 
+    [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
+  ; 
   simple_tactic:
     [ [ 
       (* Basic tactics *)
@@ -415,8 +418,7 @@ GEXTEND Gram
       | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
       | IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta -> 
 	  TacMove (true,id1,id2)
-      | IDENT "rename"; id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> 
-	  TacRename (id1,id2)
+      | IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
 
       (* Constructors *)
       | IDENT "left"; bl = with_bindings -> TacLeft bl
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d4fa5163ed..b07213fe98 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -782,10 +782,14 @@ and pr_atom1 = function
       hov 1
         (str "move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
 	 str "after" ++ brk (1,1) ++ pr_ident id2)
-  | TacRename (id1,id2) ->
+  | TacRename l ->
       hov 1
-        (str "rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ 
-	 str "into" ++ brk (1,1) ++ pr_ident id2)
+        (str "rename" ++ brk (1,1) ++
+         prlist_with_sep 
+	   (fun () -> str "," ++ brk (1,1))
+	   (fun (i1,i2) -> 
+	      pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2)
+	   l)
 
   (* Constructors *)
   | TacLeft l -> hov 1 (str "left" ++ pr_bindings l)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index c78e842ec0..8c45d95b30 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -166,7 +166,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacClear of bool * 'id list
   | TacClearBody of 'id list
   | TacMove of bool * 'id * 'id
-  | TacRename of 'id * 'id
+  | TacRename of ('id *'id) list
 
   (* Constructors *)
   | TacLeft of 'constr bindings
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 2049eb0f6a..68cd194799 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -205,8 +205,11 @@ let thin_body_no_check ids gl =
 let move_hyp_no_check with_dep id1 id2 gl = 
   refiner (Prim (Move (with_dep,id1,id2))) gl
 
-let rename_hyp_no_check id1 id2 gl = 
-  refiner (Prim (Rename (id1,id2))) gl
+let rec rename_hyp_no_check l gl = match l with 
+  | [] -> tclIDTAC gl 
+  | (id1,id2)::l -> 
+      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
@@ -234,7 +237,7 @@ let convert_hyp d      = with_check (convert_hyp_no_check d)
 let thin l             = with_check (thin_no_check l)
 let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
-let rename_hyp id id'  = with_check (rename_hyp_no_check id id')
+let rename_hyp l       = with_check (rename_hyp_no_check l)
 
 (* Pretty-printers *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 817f934db7..1d0cfe0d66 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -132,7 +132,7 @@ val convert_hyp_no_check      : named_declaration -> tactic
 val thin_no_check             : identifier list -> tactic
 val thin_body_no_check        : identifier list -> tactic
 val move_hyp_no_check         : bool -> identifier -> identifier -> tactic
-val rename_hyp_no_check       : identifier -> identifier -> tactic
+val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
@@ -150,7 +150,7 @@ val convert_hyp      : named_declaration -> tactic
 val thin             : identifier list -> tactic
 val thin_body        : identifier list -> tactic
 val move_hyp         : bool -> identifier -> identifier -> tactic
-val rename_hyp       : identifier -> identifier -> tactic
+val rename_hyp       : (identifier*identifier) list -> tactic
 
 (*s Tactics handling a list of goals. *)
 
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. *)