diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e06997029d..1d594aa7c9 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -366,6 +366,9 @@ let refine_tac simple {Glob_term.closure=closure;term=term} = TACTIC EXTEND refine | [ "refine" uconstr(c) ] -> [ refine_tac false c ] +END + +TACTIC EXTEND simple_refine | [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ] END |