aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 17:10:23 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 17:10:23 +0100
commitdffc6a20eb1a0636904164e00b5963ed96f774c4 (patch)
tree138b1c0a86f27cc3d29a65b77d7ca0335cd1dbcd /toplevel/vernac.mli
parentb3a8761790c0905aad8e5d3102fab606fe5e7fd6 (diff)
parent2a64471512ee7dcd6d6c65cd5a792344628616f0 (diff)
Merge PR #6736: [toplevel] Move beautify to its own pass.
Diffstat (limited to 'toplevel/vernac.mli')
-rw-r--r--toplevel/vernac.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index e909ada1e..ca825197b 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -26,5 +26,5 @@ val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.l
(** [load_vernac echo sid file] Loads [file] on top of [sid], will
echo the commands if [echo] is set. Callers are expected to handle
and print errors in form of exceptions. *)
-val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool ->
+val load_vernac : time:bool -> echo:bool -> check:bool -> interactive:bool ->
state:State.t -> string -> State.t