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 /tactics/tacticals.ml | |
| parent | fcef4f7d643d40cb652580e507d7bda914e8b9f2 (diff) | |
Export missing tacticals.
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 3 |
1 files changed, 3 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|] |