diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-03-22 17:55:20 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-03-22 17:57:25 +0100 |
| commit | ff8438b9930ad21b625a02e9c172c8293556f3cc (patch) | |
| tree | b9becd990c4448a998eb1772733b17d1a51b7373 /coq/coq-abbrev.el | |
| parent | 62ec846fcaaef8f3ae94302cbef2972f88a0804f (diff) | |
Added support for future new options (trunk).
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 4 |
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]) |