From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 toplevel/coqloop.mli | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

(limited to 'toplevel/coqloop.mli')

diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index e40353e0..bbb9b138 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -1,21 +1,24 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Pp
-
 (** 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. *)
 
 type input_buffer = {
-  mutable prompt : unit -> string;
-  mutable str : string; (** buffer of already read characters *)
+  mutable prompt : Stm.doc -> string;
+  mutable str : Bytes.t; (** buffer of already read characters *)
   mutable len : int;    (** number of chars in the buffer *)
   mutable bols : int list; (** offsets in str of begining of lines *)
   mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
@@ -26,16 +29,14 @@ type input_buffer = {
 val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
-(** Toplevel error explanation, dealing with locations, Drop, Ctrl-D
-  May raise only the following exceptions: [Drop] and [End_of_input],
-  meaning we get out of the Coq loop. *)
-
-val print_toplevel_error : Exninfo.iexn -> std_ppcmds
+(** Toplevel feedback printer. *)
+val coqloop_feed : Feedback.feedback -> unit
 
 (** Parse and execute one vernac command. *)
-
-val do_vernac : unit -> unit
+val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t
 
 (** Main entry point of Coq: read and execute vernac commands. *)
+val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t
 
-val loop : unit -> unit
+(** Last document seen after `Drop` *)
+val drop_last_doc : Vernac.State.t option ref
-- 
cgit v1.2.3