diff options
Diffstat (limited to 'toplevel/coqloop.mli')
-rw-r--r-- | toplevel/coqloop.mli | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 39a9de4f8..5c07a8bf3 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -10,9 +10,6 @@ (** The Coq toplevel loop. *) -(** -emacs option: printing includes emacs tags. *) -val print_emacs : bool ref - (** A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -30,10 +27,11 @@ val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) -val coqloop_feed : Feedback.feedback -> unit - -(** Main entry point of Coq: read and execute vernac commands. *) -val loop : state:Vernac.State.t -> Vernac.State.t +val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit (** Last document seen after `Drop` *) val drop_last_doc : Vernac.State.t option ref +val drop_args : Coqargs.coq_cmdopts option ref + +(** Main entry point of Coq: read and execute vernac commands. *) +val loop : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit |