diff options
| author | Enrico Tassi | 2013-12-29 18:56:12 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-05 16:55:58 +0100 |
| commit | 8e57267d4a08103506ebd6dd99b21c1f13813461 (patch) | |
| tree | ac4db1169f551300670d700dc456eac314e333b6 /toplevel | |
| parent | 2265dfad7543f0abce7e50751c650f8e5fb92683 (diff) | |
Fix coqc -time (Closes: 3201)
Diffstat (limited to 'toplevel')
| -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 } |