diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/coretactics.ml4 | 4 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 2d1220385a..28ff6df838 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -141,10 +141,10 @@ END (** Specialize *) TACTIC EXTEND specialize - [ "specialize" open_constr_with_bindings(c) ] -> [ + [ "specialize" constr_with_bindings(c) ] -> [ Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) ] -| [ "specialize" open_constr_with_bindings(c) "as" intropattern(ipat) ] -> [ +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) ] END diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index a3b3fae0b3..bd48614dbc 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -190,7 +190,7 @@ let onSomeWithHoles tac = function | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) TACTIC EXTEND contradiction - [ "contradiction" open_constr_with_bindings_opt(c) ] -> + [ "contradiction" constr_with_bindings_opt(c) ] -> [ onSomeWithHoles contradiction c ] END |