diff options
Diffstat (limited to 'ltac/extratactics.ml4')
| -rw-r--r-- | ltac/extratactics.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 60ce59ed9..725f2a534 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -144,6 +144,10 @@ TACTIC EXTEND einjection_as | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> [ mytclWithHoles (injClause (Some ipat)) true c ] END +TACTIC EXTEND simple_injection +| [ "simple" "injection" ] -> [ simpleInjClause false None ] +| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ] +END let injHyp id = Proofview.tclEVARMAP >>= fun sigma -> |