aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-abbrev.el
diff options
context:
space:
mode:
authorGravatar Tej Chajed <tchajed@mit.edu>2016-08-15 22:05:21 -0400
committerGravatar Tej Chajed <tchajed@mit.edu>2016-08-15 22:05:21 -0400
commitac69cdf056f0ee424c076d09f3848a0574f3ce83 (patch)
tree1aed347d26db884f7d24e24ac74cd4456461b946 /coq/coq-abbrev.el
parenta7c5e29ba9a6364e851fd4aa0924395c59cb324e (diff)
Add Set Printing Universes to options menu
Diffstat (limited to 'coq/coq-abbrev.el')
-rw-r--r--coq/coq-abbrev.el2
1 files changed, 2 insertions, 0 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index f23ac786..9432bd1b 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -196,6 +196,8 @@ It was constructed with `proof-defstringset-fn'.")
["Unset Printing Coercions" coq-unset-printing-coercions t]
["Set Printing Synth" coq-set-printing-synth t]
["Unset Printing Synth" coq-unset-printing-synth t]
+ ["Set Printing Universes" coq-set-printing-universes t]
+ ["Unset Printing Universes" coq-unset-printing-universes t]
["Set Printing Wildcards" coq-set-printing-wildcards t]
["Unset Printing Wildcards" coq-unset-printing-wildcards t]
["Set Printing Width" coq-ask-adapt-printing-width-and-show t])