diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-04-26 11:57:58 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-04 11:13:49 +0200 |
| commit | 1fe73e6af81759fa8b78c8660745492ed886d477 (patch) | |
| tree | 4847f56a199aa1f2cd433b3f0c1d791563634fbe /ide/coq.mli | |
| parent | 773d95f915996b581b7ea82d9193197649c951a0 (diff) | |
Adding an option "Printing Unfocused".
Off by default.
+ small refactoring of emacs hacks in printer.ml.
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 2 |
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. *) |