14 files changed, 5 insertions, 49 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e64dcb62c..530213b7c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -209,7 +209,6 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacDo of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacTimeout of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
-  | TacTime of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacRepeat of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacProgress of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacShowHyps of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
diff --git a/lib/system.ml b/lib/system.ml
index 4188eb2b4..6c357ee36 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -279,19 +279,3 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
   str "," ++
   real (round (sstop -. sstart)) ++ str "s" ++
   str ")"
-
-let with_time time f x =
-  let tstart = get_time() in
-  let msg = if time then "" else "Finished transaction in " in
-  try
-    let y = f x in
-    let tend = get_time() in
-    let msg2 = if time then "" else " (successful)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
-    y
-  with e ->
-    let tend = get_time() in
-    let msg = if time then "" else "Finished failing transaction in " in
-    let msg2 = if time then "" else " (failure)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
-    raise e
diff --git a/lib/system.mli b/lib/system.mli
index 9cfb1456f..2e286a40c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -67,5 +67,3 @@ type time
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.std_ppcmds
-
-val with_time : bool -> ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index fa352f8bf..f70a865d7 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -64,7 +64,6 @@ GEXTEND Gram
       [ IDENT "try"; ta = tactic_expr -> TacTry ta
       | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
       | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
-      | IDENT "time"; ta = tactic_expr -> TacTime ta
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
       | IDENT "once"; ta = tactic_expr -> TacOnce ta
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 9df9446c3..f6c25d069 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -865,9 +865,6 @@ let rec pr_tac inherited tac =
       hov 1 (str "timeout " ++ pr_or_var int n ++ spc () ++
              pr_tac (ltactical,E) t),
       ltactical
-  | TacTime t ->
-      hov 1 (str "time " ++ pr_tac (ltactical,E) t),
-      ltactical
   | TacRepeat t ->
       hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t),
       ltactical
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index da1937ef3..c478bd663 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 df833a04f..6a2d81511 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 8139d3026..4d4e4470c 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. *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 033e00433..f68f75359 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -613,8 +613,6 @@ and intern_tactic_seq onlytac ist = function
   | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac)
   | TacTimeout (n,tac) ->
       ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac)
-  | TacTime tac ->
-      ist.ltacvars, TacTime (intern_tactic onlytac ist tac)
   | TacOr (tac1,tac2) ->
       ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
   | TacOnce tac ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b70f21431..c749e2d72 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1023,7 +1023,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
   | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
-  | TacTime tac -> Tacticals.New.tclTIME (interp_tactic ist tac)
   | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac)
   | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac)
   | TacOr (tac1,tac2) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 8ab63c161..4dd4b0aa8 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -230,7 +230,6 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
   | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
   | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
-  | TacTime tac -> TacTime (subst_tactic subst tac)
   | TacTry tac -> TacTry (subst_tactic subst tac)
   | TacInfo tac -> TacInfo (subst_tactic subst tac)
   | TacRepeat tac -> TacRepeat (subst_tactic subst tac)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 267a34754..fcce6e5eb 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -467,9 +467,6 @@ module New = struct
         | e -> Proofview.tclZERO e
       end
 
-  let tclTIME t =
-    Proofview.tclTIME t
-
   let nthDecl m gl =
     let hyps = Proofview.Goal.hyps gl in
     try
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 705a7e2cc..48fd44b4a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -212,7 +212,6 @@ module New : sig
   val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic
 
   val tclTIMEOUT : int -> unit tactic -> unit tactic
-  val tclTIME : 'a tactic -> 'a tactic
 
   val nLastDecls  : [ `NF ] Proofview.Goal.t -> int -> named_context
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5e829a2d9..1d05f4e62 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1965,7 +1965,11 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacTime v ->
-        System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v;
+	let tstart = System.get_time() in
+        aux_list ?locality ?polymorphism isprogcmd v;
+	let tend = System.get_time() in
+	let msg = if !Flags.time then "" else "Finished transaction in " in
+        msg_info (str msg ++ System.fmt_time_difference tstart tend)
     | VernacLoad (_,fname) -> vernac_load (aux false) fname
     | c -> 
         check_vernac_supports_locality c locality;