Removing "rename" from the tactic AST.

6 files changed, 16 insertions, 23 deletions

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) ->