diff options
Diffstat (limited to 'toplevel/vernac.mli')
| -rw-r--r-- | toplevel/vernac.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 3c09139ba..8f1fbc54f 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -48,3 +48,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 |