aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2017-03-22 17:55:20 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2017-03-22 17:57:25 +0100
commitff8438b9930ad21b625a02e9c172c8293556f3cc (patch)
treeb9becd990c4448a998eb1772733b17d1a51b7373
parent62ec846fcaaef8f3ae94302cbef2972f88a0804f (diff)
Added support for future new options (trunk).
-rw-r--r--coq/coq-abbrev.el4
-rw-r--r--coq/coq-syntax.el46
-rw-r--r--coq/coq.el4
3 files changed, 33 insertions, 21 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])
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5844be74..0b86d8fe 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -706,22 +706,26 @@ so for the following reasons:
("Set Nonrecursive Elimination Schemes" nil "Set Nonrecursive Elimination Schemes" t "Set Nonrecursive\\s-+Elimination\\s-+Schemes")
("Set Parsing Explicit" nil "Set Parsing Explicit" t "Set Parsing\\s-+Explicit")
("Set Primitive Projections" nil "Set Primitive Projections" t "Set Primitive\\s-+Projections")
- ("Set Printing All" nil "Set Printing All" t "Set Printing\\s-+All")
- ("Set Printing Coercions" nil "Set Printing Coercions" t "Set Printing\\s-+Coercions")
- ("Set Printing Depth" nil "Set Printing Depth" t "Set Printing\\s-+Depth")
- ("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set Printing\\s-+Existential\\s-+Instances")
- ("Set Printing Implicit" nil "Set Printing Implicit" t "Set Printing\\s-+Implicit")
- ("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set Printing\\s-+Implicit\\s-+Defensive")
- ("Set Printing Matching" nil "Set Printing Matching" t "Set Printing\\s-+Matching")
- ("Set Printing Notations" nil "Set Printing Notations" t "Set Printing\\s-+Notations")
- ("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility")
- ("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Parameters")
- ("Set Printing Projections" nil "Set Printing Projections" t "Set Printing\\s-+Projections")
- ("Set Printing Records" nil "Set Printing Records" t "Set Printing\\s-+Records")
- ("Set Printing Synth" nil "Set Printing Synth" t "Set Printing\\s-+Synth")
- ("Set Printing Universes" nil "Set Printing Universes" t "Set Printing\\s-+Universes")
- ("Set Printing Width" nil "Set Printing Width" t "Set Printing\\s-+Width")
- ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set Printing\\s-+Wildcard")
+ ("Set Printing All" nil "Set Printing All" t "Set\\s-+Printing\\s-+All")
+ ("Set Printing Coercions" nil "Set Printing Coercions" t "Set\\s-+Printing\\s-+Coercions")
+ ("Set Printing Compact Contexts" nil "Set Printing Compact Contexts" t "Set\\s-+Printing\\s-+Compact\\s-+Contexts")
+ ("Set Printing Depth" nil "Set Printing Depth" t "Set\\s-+Printing\\s-+Depth")
+ ("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set\\s-+Printing\\s-+Existential\\s-+Instances")
+ ("Set Printing Goal Tags" nil "Set Printing Goal Tags" t "Set\\s-+Printing\\s-+Goal\\s-+Tags")
+ ("Set Printing Goal Names" nil "Set Printing Goal Names" t "Set\\s-+Printing\\s-+Goal\\s-+Names")
+ ("Set Printing Implicit" nil "Set Printing Implicit" t "Set\\s-+Printing\\s-+Implicit")
+ ("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set\\s-+Printing\\s-+Implicit\\s-+Defensive")
+ ("Set Printing Matching" nil "Set Printing Matching" t "Set\\s-+Printing\\s-+Matching")
+ ("Set Printing Notations" nil "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations")
+ ("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility")
+ ("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Parameters")
+ ("Set Printing Projections" nil "Set Printing Projections" t "Set\\s-+Printing\\s-+Projections")
+ ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records")
+ ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth")
+ ("Set Printing Unfocused" nil "Set Printing Unfocused" t "Set\\s-+Printing\\s-+Unfocused")
+ ("Set Printing Universes" nil "Set Printing Universes" t "Set\\s-+Printing\\s-+Universes")
+ ("Set Printing Width" nil "Set Printing Width" t "Set\\s-+Printing\\s-+Width")
+ ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard")
("Set Program Mode" nil "Set Program Mode" t "Set Program\\s-+Mode")
("Set Proof Using Clear Unused" nil "Set Proof Using Clear Unused" t "Set Proof\\s-+Using\\s-+Clear\\s-+Unused")
("Set Record Elimination Schemes" nil "Set Record Elimination Schemes" t "Set Record\\s-+Elimination\\s-+Schemes")
@@ -762,11 +766,11 @@ so for the following reasons:
("Set Silent" nil "Set Silent" t "Set Silent")
("Set Undo" nil "Set Undo" t "Set Undo")
("Set Search Blacklist" nil "Set Search Blacklist" t "Set Search\\s-+Blacklist")
- ("Set Printing Coercion" nil "Set Printing Coercion" t "Set Printing\\s-+Coercion")
- ("Set Printing If" nil "Set Printing If" t "Set Printing\\s-+If")
- ("Set Printing Let" nil "Set Printing Let" t "Set Printing\\s-+Let")
- ("Set Printing Record" nil "Set Printing Record" t "Set Printing\\s-+Record")
- ("Set Printing Constructor" nil "Set Printing Constructor" t "Set Printing\\s-+Constructor")
+ ("Set Printing Coercion" nil "Set Printing Coercion" t "Set\\s-+Printing\\s-+Coercion")
+ ("Set Printing If" nil "Set Printing If" t "Set\\s-+Printing\\s-+If")
+ ("Set Printing Let" nil "Set Printing Let" t "Set\\s-+Printing\\s-+Let")
+ ("Set Printing Record" nil "Set Printing Record" t "Set\\s-+Printing\\s-+Record")
+ ("Set Printing Constructor" nil "Set Printing Constructor" t "Set\\s-+Printing\\s-+Constructor")
("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations")
("Local Strategy" nil "Local Strategy # [#]." t "Local\\s-+Strategy")
("Strategy" nil "Strategy # [#]." t "Strategy")
diff --git a/coq/coq.el b/coq/coq.el
index 0c366df5..d7177044 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1367,6 +1367,10 @@ 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-compact-contexts "Set Printing Compact Contexts.")
+(proof-definvisible coq-unset-printing-compact-contexts "Unset Printing Compact Contexts.")
+(proof-definvisible coq-set-printing-unfocused "Set Printing Unfocused.")
+(proof-definvisible coq-unset-printing-unfocused "Unset Printing Unfocused.")
(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.")