diff options
| author |  Tej Chajed <tchajed@mit.edu> | 2016-08-15 22:05:21 -0400 |
|---|---|---|
| committer | Tej Chajed <tchajed@mit.edu> | 2016-08-15 22:05:21 -0400 |
| commit | ac69cdf056f0ee424c076d09f3848a0574f3ce83 (patch) | |
| tree | 1aed347d26db884f7d24e24ac74cd4456461b946 /coq/coq.el | |
| parent | a7c5e29ba9a6364e851fd4aa0924395c59cb324e (diff) | |
Add Set Printing Universes to options menu
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -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 |