diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 13 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 1 |
3 files changed, 0 insertions, 17 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index da1937ef3d..c478bd6635 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -579,19 +579,6 @@ let tclTIMEOUT n t = Proof.ret res | Util.Inr e -> tclZERO e -let tclTIME t = - let (>>=) = Proof.bind in - let (>>) = Proof.seq in - let t = Proof.lift (Proofview_monad.NonLogical.ret ()) >> t in - Proof.current >>= fun env -> - Proof.get >>= fun initial -> - Proof.lift begin - Proofview_monad.NonLogical.time !Flags.time (Proof.run t env initial) - end >>= function ((res,s),m) -> - Proof.set s >> - Proof.put m >> - Proof.ret res - let mark_as_unsafe = Proof.put (false,([],[])) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index df833a04ff..6a2d815114 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -261,9 +261,6 @@ exception Timeout In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic -(** [tclTIME t] displays time for each atomic call to t *) -val tclTIME : 'a tactic -> 'a tactic - (** [mark_as_unsafe] signals that the current tactic is unsafe. *) val mark_as_unsafe : unit tactic diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index 8139d3026b..4d4e4470c0 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -38,7 +38,6 @@ module NonLogical : sig val raise : exn -> 'a t val catch : 'a t -> (exn -> 'a t) -> 'a t val timeout : int -> 'a t -> 'a t - val time : bool -> 'a t -> 'a t (* [run] performs effects. *) |