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

---
 ide/coq.mli | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

(limited to 'ide/coq.mli')

diff --git a/ide/coq.mli b/ide/coq.mli
index 8a1fa3ed..40a6dea8 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  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)         *)
 (************************************************************************)
 
 (** Coq : Interaction with the Coq toplevel *)
@@ -115,15 +117,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
 type 'a query = 'a Interface.value task
 (** A type abbreviation for coqtop specific answers *)
 
-val add        : ?logger:Ideutils.logger ->
-                 Interface.add_sty        -> Interface.add_rty query
+val add        : Interface.add_sty        -> Interface.add_rty query
 val edit_at    : Interface.edit_at_sty    -> Interface.edit_at_rty query
-val query      : ?logger:Ideutils.logger ->
-                 Interface.query_sty      -> Interface.query_rty query
-val status     : ?logger:Ideutils.logger ->
-                 Interface.status_sty     -> Interface.status_rty query
-val goals      : ?logger:Ideutils.logger ->
-                 Interface.goals_sty      -> Interface.goals_rty query
+val query      : Interface.query_sty      -> Interface.query_rty query
+val status     : Interface.status_sty     -> Interface.status_rty query
+val goals      : Interface.goals_sty      -> Interface.goals_rty query
 val evars      : Interface.evars_sty      -> Interface.evars_rty query
 val hints      : Interface.hints_sty      -> Interface.hints_rty query
 val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
@@ -143,7 +141,8 @@ sig
   val bool_items : bool_descr list
 
   val set : t -> bool -> unit
-  val set_printing_width : int -> unit
+
+  val printing_unfocused: unit -> bool
 
   (** [enforce] transmits to coq the current option values.
       It is also called by [goals] and [evars] above. *)
@@ -173,3 +172,7 @@ val check_connection : string list -> unit
     may terminate coqide in case of trouble *)
 
 val interrupter : (int -> unit) ref
+val save_all : (unit -> unit) ref
+
+(* Flags to be used for ideslave *)
+val ideslave_coqtop_flags : string option ref
-- 
cgit v1.2.3