aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index ab8c12a6f..e8e2f5239 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -140,6 +140,8 @@ sig
val set : t -> bool -> unit
+ val printing_unfocused: unit -> bool
+
(** [enforce] transmits to coq the current option values.
It is also called by [goals] and [evars] above. *)