diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 9 |
2 files changed, 0 insertions, 17 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 59fd8b37d6..81700986ea 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -43,12 +43,8 @@ let tclTHENS = Refiner.tclTHENS let tclTHENSV = Refiner.tclTHENSV let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn let tclTHENSLASTn = Refiner.tclTHENSLASTn -let tclTHENFIRSTn = Refiner.tclTHENFIRSTn -let tclTHENLASTn = Refiner.tclTHENLASTn let tclREPEAT = Refiner.tclREPEAT -let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN let tclFIRST = Refiner.tclFIRST -let tclSOLVE = Refiner.tclSOLVE let tclTRY = Refiner.tclTRY let tclCOMPLETE = Refiner.tclCOMPLETE let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE @@ -58,10 +54,6 @@ let tclDO = Refiner.tclDO let tclPROGRESS = Refiner.tclPROGRESS let tclSHOWHYPS = Refiner.tclSHOWHYPS let tclTHENTRY = Refiner.tclTHENTRY -let tclIFTHENELSE = Refiner.tclIFTHENELSE -let tclIFTHENSELSE = Refiner.tclIFTHENSELSE -let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE -let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST (************************************************************************) (* Tacticals applying on hypotheses *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 201b7801c3..a9ccda527f 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -31,13 +31,9 @@ val tclTHENLAST : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic val tclTHENSV : tactic -> tactic array -> tactic val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic -val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -val tclTHENFIRSTn : tactic -> tactic array -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic @@ -49,11 +45,6 @@ val tclSHOWHYPS : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic - (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic |