diff options
Diffstat (limited to 'ide/coqide/coq.ml')
| -rw-r--r-- | ide/coqide/coq.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 1167b8199e..b8228df2aa 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -550,6 +550,7 @@ struct let existential = BoolOpt ["Printing"; "Existential"; "Instances"] let universes = BoolOpt ["Printing"; "Universes"] let unfocused = BoolOpt ["Printing"; "Unfocused"] + let goal_names = BoolOpt ["Printing"; "Goal"; "Names"] let diff = StringOpt ["Diffs"] type 'a descr = { opts : 'a t list; init : 'a; label : string } @@ -568,7 +569,8 @@ struct { opts = [universes]; init = false; label = "Display _universe levels" }; { opts = [all_basic;existential;universes]; init = false; label = "Display all _low-level contents" }; - { opts = [unfocused]; init = false; label = "Display _unfocused goals" } + { opts = [unfocused]; init = false; label = "Display _unfocused goals" }; + { opts = [goal_names]; init = false; label = "Display _goal names" } ] let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" } |