14 files changed, 49 insertions, 5 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 530213b7c..e64dcb62c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -209,6 +209,7 @@ 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 6c357ee36..4188eb2b4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -279,3 +279,19 @@ 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 2e286a40c..9cfb1456f 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -67,3 +67,5 @@ 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 f70a865d7..fa352f8bf 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -64,6 +64,7 @@ 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 f6c25d069..9df9446c3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -865,6 +865,9 @@ 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 c478bd663..da1937ef3 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -579,6 +579,19 @@ 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 6a2d81511..df833a04f 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -261,6 +261,9 @@ 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 4d4e4470c..8139d3026 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -38,6 +38,7 @@ 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 f68f75359..033e00433 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -613,6 +613,8 @@ 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 c749e2d72..b70f21431 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1023,6 +1023,7 @@ 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 4dd4b0aa8..8ab63c161 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -230,6 +230,7 @@ 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 fcce6e5eb..267a34754 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -467,6 +467,9 @@ 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 48fd44b4a..705a7e2cc 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -212,6 +212,7 @@ 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 1d05f4e62..5e829a2d9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1965,11 +1965,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacTime 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)
+        System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v;
     | VernacLoad (_,fname) -> vernac_load (aux false) fname
     | c -> 
         check_vernac_supports_locality c locality;