aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.mli
diff options
context:
space:
mode:
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