diff options
| author | Pierre-Marie Pédrot | 2020-05-02 14:09:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | 87e811844fa980200cd23eea2b51fd525152e134 (patch) | |
| tree | c0f45cb29cb206c7082e92851ef55f149bd4bfd7 | |
| parent | fcef4f7d643d40cb652580e507d7bda914e8b9f2 (diff) | |
Export missing tacticals.
| -rw-r--r-- | tactics/tacticals.ml | 3 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 8f6844079b..07f9def2c8 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -368,6 +368,9 @@ module New = struct Proofview.Unsafe.tclNEWGOALS tl <*> Proofview.tclUNIT ans + let tclTHENSLASTn t1 repeat l = + tclTHENS3PARTS t1 [||] repeat l + let tclTHENLASTn t1 l = tclTHENS3PARTS t1 [||] (tclUNIT()) l let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 9ec558f1ad..01565169ca 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -180,6 +180,7 @@ module New : sig middle. Raises an error if the number of resulting subgoals is strictly less than [n+m] *) val tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic + val tclTHENSLASTn : unit tactic -> unit tactic -> unit tactic array -> unit tactic val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic |