Revert "time tac" (committed by mistake).

This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.

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. *)