diff options
| author | Maxime Dénès | 2015-12-16 21:33:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-12-16 21:33:03 +0100 |
| commit | 793cf771e18be3d44d3fcf89998dec50fb8229f3 (patch) | |
| tree | d0d33aa6ae41d95d8c8c5b0e64c507a99eaf1ace | |
| parent | b8d1e84e9326df34383e5e5c8c5842cb7013b935 (diff) | |
FIx parsing of tactic "simple refine".
| -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 |