diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 3a1d87787..cd45e2fcd 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -519,6 +519,7 @@ struct let all_basic = ["Printing"; "All"] let existential = ["Printing"; "Existential"; "Instances"] let universes = ["Printing"; "Universes"] + let unfocused = ["Printing"; "Unfocused"] type bool_descr = { opts : t list; init : bool; label : string } @@ -534,7 +535,8 @@ struct label = "Display _existential variable instances" }; { opts = [universes]; init = false; label = "Display _universe levels" }; { opts = [all_basic;existential;universes]; init = false; - label = "Display all _low-level contents" } + label = "Display all _low-level contents" }; + { opts = [unfocused]; init = false; label = "Display _unfocused goals" } ] (** The current status of the boolean options *) @@ -549,6 +551,8 @@ struct let _ = reset () + let printing_unfocused () = Hashtbl.find current_state unfocused + (** Transmitting options to coqtop *) let enforce h k = |