aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-abbrev.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-abbrev.el')
-rw-r--r--coq/coq-abbrev.el4
1 files changed, 4 insertions, 0 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 2b318dea..062f7580 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -289,10 +289,14 @@ It was constructed with `proof-defstringset-fn'.")
["Unset Printing Implicit" coq-unset-printing-implicit t]
["Set Printing Coercions" coq-set-printing-coercions t]
["Unset Printing Coercions" coq-unset-printing-coercions t]
+ ["Set Printing Compact Contexts" coq-set-printing-implicit t]
+ ["Unset Printing Compact Contexts" coq-unset-printing-implicit 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 Unfocused" coq-set-printing-unfocused t]
+ ["Unset Printing Unfocused" coq-unset-printing-unfocused 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])