diff options
Diffstat (limited to 'plugins/ltac/coretactics.mlg')
| -rw-r--r-- | plugins/ltac/coretactics.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index 01817dc8f9..2159c05f80 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -150,7 +150,7 @@ TACTIC EXTEND specialize | [ "specialize" constr_with_bindings(c) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) } -| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> { +| [ "specialize" constr_with_bindings(c) "as" simple_intropattern(ipat) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) } END |