diff options
| -rw-r--r-- | toplevel/vernac.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 3 |
2 files changed, 1 insertions, 6 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d9c23c0ad6..abf58df459 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -47,8 +47,6 @@ let is_reset = function (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) -let time = ref false - let display_cmd_header loc com = let shorten s = try (String.sub s 0 30)^"..." with Invalid_argument _ -> s in @@ -274,7 +272,7 @@ let rec vernac_com verbosely checknav (loc,com) = checknav loc com; if do_beautify () then pr_new_syntax loc (Some com); if !Flags.time then display_cmd_header loc com; - let com = if !time then VernacTime com else com in + let com = if !Flags.time then VernacTime com else com in interp com with reraise -> let reraise = Errors.push reraise in diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d185719909..f3988d53ed 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -39,9 +39,6 @@ val compile : bool -> string -> unit val is_navigation_vernac : Vernacexpr.vernac_expr -> bool -(** Should we display timings for each command ? *) -val time : bool ref - (** Has an exception been annotated with some file locations ? *) type location_files = { outer : string; inner : string } |