From ff8438b9930ad21b625a02e9c172c8293556f3cc Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 22 Mar 2017 17:55:20 +0100 Subject: Added support for future new options (trunk). --- coq/coq-abbrev.el | 4 ++++ coq/coq-syntax.el | 46 +++++++++++++++++++++++++--------------------- coq/coq.el | 4 ++++ 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.") -- cgit v1.2.3