diff options
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 8cc556c62a..00ce4da8d5 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -28,6 +28,7 @@ open Tacexpr val tclNORMEVAR : tactic val tclIDTAC : tactic val tclIDTAC_MESSAGE : std_ppcmds -> tactic +val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENSEQ : tactic list -> tactic @@ -57,8 +58,10 @@ val tclNOTSAMEGOAL : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclNTH_HYP : int -> (constr -> tactic) -> tactic +val tclNTH_DECL : int -> (named_declaration -> tactic) -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic val tclLAST_HYP : (constr -> tactic) -> tactic +val tclLAST_DECL : (named_declaration -> tactic) -> tactic val tclLAST_NHYPS : int -> (identifier list -> tactic) -> tactic val tclTRY_sign : (constr -> tactic) -> named_context -> tactic val tclTRY_HYPS : (constr -> tactic) -> tactic |