aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.mli')
-rw-r--r--toplevel/coqloop.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 39a9de4f8..6d9867fb9 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -30,7 +30,7 @@ val top_buffer : input_buffer
val set_prompt : (unit -> string) -> unit
(** Toplevel feedback printer. *)
-val coqloop_feed : Feedback.feedback -> unit
+val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit
(** Main entry point of Coq: read and execute vernac commands. *)
val loop : state:Vernac.State.t -> Vernac.State.t