diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 321d50df38..de4d589eee 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -142,7 +142,10 @@ END TACTIC EXTEND specialize [ "specialize" constr_with_bindings(c) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false c Tactics.specialize + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) + ] +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) ] END |