aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-15 04:15:55 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-23 19:30:17 +0100
commited09ae7a473a99c914f2af64d3387d9190e85849 (patch)
treee5b51993dc0602eb1fa985d293d82c03d286ec86 /toplevel/coqloop.mli
parentdea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff)
[flags] Move global time flag into an attribute.
One less global flag.
Diffstat (limited to 'toplevel/coqloop.mli')
-rw-r--r--toplevel/coqloop.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 46934f326..09240ec82 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,8 +32,8 @@ val coqloop_feed : Feedback.feedback -> unit
(** Parse and execute one vernac command. *)
-val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
(** Main entry point of Coq: read and execute vernac commands. *)
-val loop : Stm.doc -> Stm.doc
+val loop : time:bool -> Stm.doc -> Stm.doc