From ac69cdf056f0ee424c076d09f3848a0574f3ce83 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Mon, 15 Aug 2016 22:05:21 -0400
Subject: Add Set Printing Universes to options menu

---
 coq/coq-abbrev.el | 2 ++
 coq/coq.el        | 2 ++
 2 files changed, 4 insertions(+)

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])
diff --git a/coq/coq.el b/coq/coq.el
index 59f3fb04..6df0a30c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1354,6 +1354,8 @@ goal is redisplayed."
 (proof-definvisible coq-unset-printing-synth "Unset Printing Synth.")
 (proof-definvisible coq-set-printing-coercions "Set Printing Coercions.")
 (proof-definvisible coq-unset-printing-coercions "Unset Printing Coercions.")
+(proof-definvisible coq-set-printing-universes "Set Printing Universes.")
+(proof-definvisible coq-unset-printing-universes "Unset Printing Universes.")
 (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.")
 (proof-definvisible coq-unset-printing-wildcards "Unset Printing Wildcard.")
 ; Takes an argument
-- 
cgit v1.2.3