diff options
| -rw-r--r-- | coq/coq-abbrev.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 4 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 9 |
3 files changed, 13 insertions, 2 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 87f61df6..534c013d 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -257,6 +257,8 @@ It was constructed with `proof-defstringset-fn'.") ["Unset Printing Coercions" coq-unset-printing-coercions 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 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]) @@ -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 @@ -1786,7 +1788,7 @@ Near here means PT is either inside or just aside of a comment." (defpacustom search-blacklist coq-search-blacklist-string "Strings to blacklist in requests to coq environment." :type 'string - ;;:get coq-search-blacklist-string + :get 'coq-get-search-blacklist :setting coq-set-search-blacklist) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index be29a660..40c0ef87 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4396,12 +4396,19 @@ one project you can set the option as local file variable, @ref{Using file variables}. This can be done either directly in every file or once for all files of a directory tree with a @code{.dir-local.el} file, @inforef{Directory Variables, ,emacs}. -For this case, this file should contain +The file @code{.dir-local.el} should then contain @lisp ((coq-mode . ((coq-project-filename . "myprojectfile")))) @end lisp +Note that variables set in @code{.dir-local.el} are automatically +made buffer local (such that files in different directories can +have their independent setting of @code{coq-project-filename}). +If you make complex customizations using @code{eval} in +@code{.dir-local.el}, you might want to add appropriate calls to +@code{make-local-variable}. + Documentation of the user option @code{coq-project-filename}: @c TEXI DOCSTRING MAGIC: coq-project-filename |