aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.mli')
-rw-r--r--proofs/proofview.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index cdc2db796..a1213cde2 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -235,10 +235,6 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact
backtracking in another. *)
val tclINDEPENDENT : unit tactic -> unit tactic
-(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
-val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic
-
-
(* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *)
val tclPROGRESS : 'a tactic -> 'a tactic