diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-26 18:35:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-27 19:17:37 +0200 |
| commit | 3c1c101a8757c438379441a334f31f5fe656ef55 (patch) | |
| tree | 4f029a6d586337bd25b09ce77afe7705a01c8c6f /tactics/tacticals.mli | |
| parent | a7946816d96cb66aa7d62302e8aa602a3a9f3c99 (diff) | |
Adding tacticals tclBINDFIRST/tclBINDLAST.
Design choice: Failing with an anomaly or with a catchable Ltac error
"Fail": we fail with a Fail as it was the case with the related
constrained version of tclTHENFIRST/tclTHENLAST.
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index f0ebac780..340d8fbf3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -196,8 +196,10 @@ module New : sig (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic + val tclBINDFIRST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic val tclTHENLAST : unit tactic -> unit tactic -> unit tactic + val tclBINDLAST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic (* [tclTHENS t l = t <*> tclDISPATCH l] *) val tclTHENS : unit tactic -> unit tactic list -> unit tactic (* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *) |