diff options
Diffstat (limited to 'tactics/coretactics.ml4')
| -rw-r--r-- | tactics/coretactics.ml4 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index a07069bd3..d49040fc0 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -139,3 +139,9 @@ TACTIC EXTEND esplit_with Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true) sigma [bl] ] END + +(** Intro *) + +TACTIC EXTEND intros_until + [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] +END |