From 74ddca99c649f2f8c203582a9b82bddf64fb6b52 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 22 Apr 2014 15:31:12 +0200
Subject: Removing dead code, thanks to new OCaml warnings and a bit of
 scripting.

---
 proofs/refiner.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'proofs/refiner.mli')

diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 2ea877725..f73bdaf93 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -65,10 +65,6 @@ val tclTHENSV         : tactic -> tactic array -> tactic
 (** Same with a list of tactics *)
 val tclTHENS         : tactic -> tactic list -> tactic
 
-(** [tclTHENST] is renamed [tclTHENSFIRSTn]
-val tclTHENST        : tactic -> tactic array -> tactic -> tactic
-*)
-
 (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
-- 
cgit v1.2.3