diff options
| author |  hendriktews <hendrik@askra.de> | 2016-12-15 10:25:33 +0100 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-12-15 10:25:33 +0100 |
| commit | de841653b6a5baa3cf0f5ab290531afce384ea02 (patch) | |
| tree | e3daa091475d3011542c64fd5fcd3740d8487043 | |
| parent | 93a0d1ca16fd30e89e312932008106bc5503386f (diff) | |
| parent | ac69cdf056f0ee424c076d09f3848a0574f3ce83 (diff) | |
Merge pull request #101 from tchajed/print-universes-option
Add Set Printing Universes to options menu
| -rw-r--r-- | coq/coq-abbrev.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 87f61df6..534c013d 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -257,6 +257,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]) @@ -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 |