diff options
Diffstat (limited to 'plugins/ltac/coretactics.ml4')
| -rw-r--r-- | plugins/ltac/coretactics.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 931633e1a..61525cb49 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -10,11 +10,13 @@ open Util open Locus -open Misctypes +open Tactypes open Genredexpr open Stdarg open Extraargs +open Tacarg open Names +open Logic DECLARE PLUGIN "ltac_plugin" @@ -273,15 +275,13 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Tactics.fix None n ] -| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] + [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Tactics.cofix None ] -| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] + [ "cofix" ident(id) ] -> [ Tactics.cofix id ] END (* Clear *) |