diff options
Diffstat (limited to 'ltac/coretactics.ml4')
| -rw-r--r-- | ltac/coretactics.ml4 | 6 |
1 files changed, 6 insertions, 0 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 |