diff options
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|] |