Removing "rename" from the tactic AST.

9 files changed, 16 insertions, 40 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e1d4809609..379dd59d39 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -156,9 +156,6 @@ type 'a gen_atomic_tactic_expr =
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
 
-  (* Context management *)
-  | TacRename of ('nam *'nam) list
-
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
   | TacChange of 'pat option * 'dtrm * 'nam clause_expr
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 8e37653f57..9879cfc280 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -223,6 +223,12 @@ TACTIC EXTEND move
 | [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
 END
 
+(** Rename *)
+
+TACTIC EXTEND rename
+| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ]
+END
+
 (** Revert *)
 
 TACTIC EXTEND revert
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 9a2a176cbf..e6d0a9c69c 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -236,6 +236,14 @@ ARGUMENT EXTEND hloc
 
  END
 
+let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m
+
+ARGUMENT EXTEND rename
+  TYPED AS ident * ident
+  PRINTED BY pr_rename
+| [ ident(n) "into" ident(m) ] -> [ (n, m) ]
+END
+
 (* Julien: Mise en commun des differentes version de replace with in by *)
 
 let pr_by_arg_tac _prc _prlc prtac opt_c =
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index 2118e87b11..0cf77935c2 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -16,6 +16,8 @@ val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
 val pr_orient : bool -> Pp.std_ppcmds
 
+val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
+
 val occurrences : (int list or_var) Pcoq.Gram.entry
 val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
 val pr_occurrences : int list or_var -> Pp.std_ppcmds
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index c1c7be1cc9..d39f835528 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -516,12 +516,6 @@ let rec intern_atomic lf ist x =
                Option.map (intern_or_and_intro_pattern_loc lf ist) ipats),
                Option.map (clause_app (intern_hyp_location ist)) cls)) l,
                Option.map (intern_constr_with_bindings ist) el))
-  (* Context management *)
-  | TacRename l ->
-      TacRename (List.map (fun (id1,id2) ->
-			     intern_hyp ist id1,
-			     intern_hyp ist id2) l)
-
   (* Conversion *)
   | TacReduce (r,cl) ->
       dump_glob_red_expr r;
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index c51c36538d..5ee9b0fc4d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1800,20 +1800,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
-  (* Context management *)
-  | TacRename l ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = pf_env gl in
-        let sigma = project gl in
-        let l =
-          List.map (fun (id1,id2) ->
-	    interp_hyp ist env sigma id1,
-	    interp_ident ist env sigma (snd id2)) l
-        in
-        name_atomic ~env
-          (TacRename l)
-          (Tactics.rename_hyp l)
-      end }
 
   (* Conversion *)
   | TacReduce (r,cl) ->
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 3c1a384ceb..2c3c76ef74 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -161,9 +161,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       let el' = Option.map (subst_glob_with_bindings subst) el in
       TacInductionDestruct (isrec,ev,(l',el'))
 
-  (* Context management *)
-  | TacRename l as x -> x
-
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (op,c,cl) ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 6e1731bb2b..36fffd74fa 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -604,9 +604,6 @@ GEXTEND Gram
       | IDENT "edestruct";  icl = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
-      (* Context management *)
-      | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
-
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
 	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 633ff18762..114410fed1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -900,17 +900,6 @@ module Make
               pr_opt pr_eliminator el
           )
 
-        (* Context management *)
-        | TacRename l ->
-          hov 1 (
-            primitive "rename" ++ brk (1,1)
-            ++ prlist_with_sep
-              (fun () -> str "," ++ brk (1,1))
-              (fun (i1,i2) ->
-                pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
-              l
-          )
-
         (* Conversion *)
         | TacReduce (r,h) ->
           hov 1 (