From 002ffc79d9c3d60afea21883703df476e18adc53 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Sep 2016 11:48:07 -0700 Subject: Add Context to coq-syntax.el --- coq/coq-syntax.el | 1 + 1 file changed, 1 insertion(+) (limited to 'coq') diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 195636a5..d6854e9a 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -431,6 +431,7 @@ so for the following reasons: ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") ("Variable" "v" "Variable #: #." t "Variable") ("Variables" "vs" "Variables # , #: #." t "Variables") + ("Context" nil "Context #, (# : #)." t "Context") ("Local Coercion" nil "Local Coercion @{id} : @{typ1} >-> @{typ2}." t "Local\\s-+Coercion") ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") ) -- cgit v1.2.3 From 6d1f608c6e7c39eff89b9461a2f4ea7ff1b19899 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 14 Jan 2017 23:27:24 +0100 Subject: Fix prooftree for Coq 8.6 In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook. --- coq/coq-system.el | 12 ++++++ coq/coq.el | 112 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 120 insertions(+), 4 deletions(-) (limited to 'coq') diff --git a/coq/coq-system.el b/coq/coq-system.el index 88ce06be..0b9b6c58 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -170,6 +170,18 @@ Returns nil if the version can't be detected." (signal 'coq-unclassifiable-version coq-version-to-use)) (t (signal (car err) (cdr err)))))))) +(defun coq--post-v86 () + "Return t if the auto-detected version of Coq is >= 8.6. +Return nil if the version cannot be detected." + (let ((coq-version-to-use (or (coq-version t) "8.5"))) + (condition-case err + (not (coq--version< coq-version-to-use "8.6")) + (error + (cond + ((equal (substring (cadr err) 0 15) "Invalid version") + (signal 'coq-unclassifiable-version coq-version-to-use)) + (t (signal (car err) (cdr err)))))))) + (defcustom coq-use-makefile nil "Whether to look for a Makefile to attempt to guess the command line. Set to t if you want this feature, but note that it is deprecated." diff --git a/coq/coq.el b/coq/coq.el index e3541b48..edf905ae 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -24,6 +24,8 @@ (defvar proof-info nil) ; dynamic scope in proof-tree-urgent-action (defvar action nil) ; dynamic scope in coq-insert-as stuff (defvar string nil) ; dynamic scope in coq-insert-as stuff + (defvar old-proof-marker nil) + ; dynamic scoq in coq-proof-tree-enable-evar-callback (defvar coq-auto-insert-as nil) ; defpacustom (defvar coq-time-commands nil) ; defpacustom (defvar coq-use-project-file t) ; defpacustom @@ -1851,14 +1853,19 @@ not finished, because Coq 8.5 lists open existential variables as (new) open subgoals. For this test we assume that `proof-marker' has not yet been moved. +The `proof-tree-urgent-action-hook' is also called for undo +commands. For those, nothing is done. + The not yet delayed output is in the region \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." ;; (message "CPTGNS start %s end %s" ;; proof-shell-delayed-output-start ;; proof-shell-delayed-output-end) - (with-current-buffer proof-shell-buffer - (let ((start proof-shell-delayed-output-start) - (end proof-shell-delayed-output-end)) + (let ((start proof-shell-delayed-output-start) + (end proof-shell-delayed-output-end) + (state (car proof-info))) + (when (> state proof-tree-last-state) + (with-current-buffer proof-shell-buffer ;; The message "All the remaining goals are on the shelf" is processed as ;; urgent message and is therefore before ;; proof-shell-delayed-output-start. We therefore need to go back to @@ -1879,7 +1886,7 @@ The not yet delayed output is in the region '(no-goals-display no-response-display proof-tree-show-subgoal)) - proof-action-list))))))))) + proof-action-list)))))))))) (add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals) @@ -1916,6 +1923,103 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." (span-start span-res))) +;; In Coq 8.6 the evar line is disabled by default because on some proofs it +;; causes a severe performance hit. The disabled evar line causes prooftree to +;; crash with a parsing error. Proof General must therefore turn on the evar +;; output with the command "Set Printing Dependent Evars Line". Of course, +;; after the proof, the evar line must be set back to what it was before the +;; proof. I therefore look in the urgent action hook if proof display is +;; switched on or off. When switched on, I test the current evar printing +;; status with the undodumented command "Test Printing Dependent Evars Line" to +;; remember if I have to switch evar printing off eventually. + +(defvar coq--proof-tree-must-disable-evars nil + "Remember if evar printing must be disabled when leaving the current proof.") + +(defun coq-proof-tree-enable-evar-callback (span) + "Callback for the evar printing status test. +This is the callback for the command ``Test Printing Dependent +Evars Line''. It checks whether evar printing was off and +remembers that fact in `coq--proof-tree-must-disable-evars'." + (with-current-buffer proof-shell-buffer + (save-excursion + ;; When the callback runs, the next item is sent to Coq already and + ;; therefore proof-marker points to the end of the next command + ;; already. proof-shell-filter-manage-output sets old-proof-marker + ;; before calling proof-shell-exec-loop, this therefore points to the + ;; end of the command of this callback. + (goto-char old-proof-marker) + (when (re-search-forward "The Printing Dependent Evars Line mode is " + nil t) + (if (looking-at "off") + (progn + ;; (message "CPTEEC evar line mode was off") + (setq coq--proof-tree-must-disable-evars t)) + ;; (message "CPTEEC evar line mode was on") + (setq coq--proof-tree-must-disable-evars nil)))))) + +(defun coq-proof-tree-insert-evar-command (cmd &optional callback) + "Insert an evar printing command at the head of `proof-action-list'." + (push (proof-shell-action-list-item + (concat cmd " Printing Dependent Evars Line.") + (if callback callback 'proof-done-invisible) + (list 'invisible)) + proof-action-list)) + +(defun coq-proof-tree-enable-evars () + "Enable the evar status line for Coq >= 8.6. +Test the status of evar printing to be able to set it back +properly after the proof and enable the evar printing." + (when (coq--post-v86) + ;; We push to proof-action-list --- therefore we need to push in reverse + ;; order! + (coq-proof-tree-insert-evar-command "Set") + (coq-proof-tree-insert-evar-command + "Test" + 'coq-proof-tree-enable-evar-callback))) + +(defun coq-proof-tree-disable-evars () + "Disable evar printing if necessary. +This function switches off evar printing after the proof, if it +was off before the proof. For undo commands, we rely on the fact +that Coq itself undos the effect of the evar printing change that +we inserted after the goal statement. We also rely on the fact +that Proof General never backtracks into the middle of a +proof. (If this would happen, Coq would switch evar printing on +and the code here would not switch it off after the proof.) + +Being called from `proof-tree-urgent-action-hook', this function +can rely on `proof-info' being dynamically bound to the last +result of `coq-proof-tree-get-proof-info'." + (when coq--proof-tree-must-disable-evars + (when (> (car proof-info) proof-tree-last-state) + (coq-proof-tree-insert-evar-command "Unset")) + (setq coq--proof-tree-must-disable-evars nil))) + +(defun coq-proof-tree-evar-display-toggle () + "Urgent action hook function for changing the evar printing status in Coq. +This function is for `proof-tree-urgent-action-hook' (which is +called only if external proof disaply is switched on). It checks +whether a proof was started or stopped and inserts commands for +enableing and disabling the evar status line for Coq 8.6 or +later. Without the evar status line being enabled, prooftree +crashes. + +Must only be called via `proof-tree-urgent-action-hook' to ensure +that the dynamic variable `proof-info' is bound to the current +result of `coq-proof-tree-get-proof-info'." + (let ((current-proof-name (cadr proof-info))) + (cond + ((and (null proof-tree-current-proof) current-proof-name) + ;; started a new proof + (coq-proof-tree-enable-evars)) + ((and proof-tree-current-proof (null current-proof-name)) + ;; finished the current proof + (coq-proof-tree-disable-evars))))) + +(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Pre-processing of input string -- cgit v1.2.3 From f487c716306913b2a02cde1bcfdcc12b81137c14 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Jan 2017 10:57:40 -0500 Subject: Add {Local ,}Axioms like {Local ,}Axiom, fix Parameters (#106) --- coq/coq-syntax.el | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'coq') diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 2f6104fe..5844be74 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -411,7 +411,9 @@ so for the following reasons: (defvar coq-decl-db '( ("Local Axiom" nil "Local Axiom # : #" t "Local\\s-+Axiom") + ("Local Axioms" nil "Local Axioms # , #: #" t "Local\\s-+Axioms") ("Axiom" "ax" "Axiom # : #" t "Axiom") + ("Axioms" "axs" "Axioms # , #: #" t "Axioms") ("Global Variable" "gv" "Global Variable #: #." t "Global\\s-+Variable") ("Global Variables" "gvs" "Global Variables # , #: #." t "Global\\s-+Variables") ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") @@ -427,7 +429,7 @@ so for the following reasons: ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") ("Parameter" "par" "Parameter #: #" t "Parameter") - ("Parameters" "par" "Parameter #: #" t "Parameters") + ("Parameters" "par" "Parameters #: #" t "Parameters") ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") ("Variable" "v" "Variable #: #." t "Variable") ("Variables" "vs" "Variables # , #: #." t "Variables") -- cgit v1.2.3 From 94439d50451ad4a3e14c705dc2774c76e6530074 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 17 Jan 2017 15:55:13 +0100 Subject: fix coqtags @psteckler I believe you have this patch already in your branch. --- coq/coqtags | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'coq') diff --git a/coq/coqtags b/coq/coqtags index 6d874e9d..76b5bcc9 100755 --- a/coq/coqtags +++ b/coq/coqtags @@ -52,7 +52,7 @@ while(<>) { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; } elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/) - { do adddecs($stmt,$1) } + { adddecs($stmt,$1); } elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/) { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; } -- cgit v1.2.3 From 77c3f2eac868f177b73d2aa59b277e40fc48fd0c Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 18 Jan 2017 22:05:37 +0100 Subject: split emergency-cleanup to handle interrupts properly (fixes #143) Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors. --- coq/coq-compile-common.el | 8 ++--- coq/coq-par-compile.el | 79 +++++++++++++++++++++++++++++++++++++---------- 2 files changed, 66 insertions(+), 21 deletions(-) (limited to 'coq') diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index af3e70a4..4b0033d1 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -42,9 +42,9 @@ Must be used together with `coq-seq-disable'." (add-hook 'proof-shell-extend-queue-hook 'coq-par-preprocess-require-commands) (add-hook 'proof-shell-signal-interrupt-hook - 'coq-par-emergency-cleanup) + 'coq-par-user-interrupt) (add-hook 'proof-shell-handle-error-or-interrupt-hook - 'coq-par-emergency-cleanup)) + 'coq-par-user-interrupt)) (defun coq-par-disable () "Disable parallel compilation. @@ -52,9 +52,9 @@ Must be used together with `coq-seq-enable'." (remove-hook 'proof-shell-extend-queue-hook 'coq-par-preprocess-require-commands) (remove-hook 'proof-shell-signal-interrupt-hook - 'coq-par-emergency-cleanup) + 'coq-par-user-interrupt) (remove-hook 'proof-shell-handle-error-or-interrupt-hook - 'coq-par-emergency-cleanup)) + 'coq-par-user-interrupt)) (defun coq-seq-enable () "Enable sequential synchronous compilation. diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 8901a008..f9b317c2 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -756,20 +756,15 @@ Used for unlocking ancestors on compilation errors." (put job 'lock-state 'unlocked))) coq--compilation-object-hash))) -(defun coq-par-emergency-cleanup () - "Emergency cleanup for parallel background compilation. -Kills all processes, unlocks ancestors, clears the queue region -and resets the internal state." - (interactive) ; needed for menu - (let (proc-killed was-busy) +(defun coq-par-kill-and-cleanup () + "Kill all background compilation, cleanup internal state and unlock ancestors. +This is the common core of `coq-par-emergency-cleanup' and +`coq-par-user-interrupt'. Returns t if there actually was a +background job that was killed." + (let (proc-killed) (when coq--debug-auto-compilation - (message "emergency cleanup")) + (message "kill all jobs and cleanup state")) (setq proc-killed (coq-par-kill-all-processes)) - (when (and (boundp 'prover-was-busy) - (or proc-killed coq--last-compilation-job - coq--compile-vio2vo-in-progress - coq--compile-vio2vo-delay-timer)) - (setq prover-was-busy t)) (setq coq-par-compilation-queue (coq-par-new-queue)) (setq coq--last-compilation-job nil) (setq coq-par-vio2vo-queue (coq-par-new-queue)) @@ -778,12 +773,62 @@ and resets the internal state." (cancel-timer coq--compile-vio2vo-delay-timer) (setq coq--compile-vio2vo-delay-timer nil)) (coq-par-unlock-all-ancestors-on-error) - (when proof-action-list - (setq proof-shell-interrupt-pending t)) - (proof-release-lock) - (proof-detach-queue) (setq proof-second-action-list-active nil) - (coq-par-init-compilation-hash))) + (coq-par-init-compilation-hash) + proc-killed)) + +(defun coq-par-emergency-cleanup () + "Emergency cleanup for errors in parallel background compilation. +This is the function that cleans everything up when some +background compilation process detected a severe error. When +`coq-compile-keep-going' is nil, all errors are severe. When +`coq-compile-keep-going' is t, coqc and some coqdep errors are +not severe. This function is also used for the user action to +kill all background compilation. + +On top of `coq-par-kill-and-cleanup', this function resets the +queue region (and thus `proof-action-list' and signals an +interrupt to the proof shell." + (interactive) ; needed for menu + (when coq--debug-auto-compilation + (message "emergency cleanup")) + (coq-par-kill-and-cleanup) + (when proof-action-list + (setq proof-shell-interrupt-pending t)) + (proof-release-lock) + (proof-detach-queue)) + +(defun coq-par-user-interrupt () + "React to a generic user interrupt with cleaning up everything. +This function cleans up background compilation when the proof +assistant died (`proof-shell-handle-error-or-interrupt-hook') or +when the user interrupted Proof General (with C-c C-c or +`proof-interrupt-process' leading to +`proof-shell-signal-interrupt-hook'). + +On top of `coq-par-kill-and-cleanup', this function only sets the +dynamic variable `prover-was-busy' to tell the proof shell that +the user actually had a reason to interrupt. However, in the +special case where `proof-action-list' is nil and +`coq--last-compilation-job' not, this function also clears the +queue region and releases the proof shell lock. This has the nice +side effect, that `proof-interrupt-process' does not send an +interrupt signal to the prover." + (let (proc-killed + (was-busy (or coq--last-compilation-job + coq--compile-vio2vo-in-progress + coq--compile-vio2vo-delay-timer))) + (when coq--debug-auto-compilation + (message "cleanup on user interrupt")) + (setq proc-killed (coq-par-kill-and-cleanup)) + (unless proof-action-list + (when coq--debug-auto-compilation + (message "clear queue region and proof shell lock")) + (proof-release-lock) + (proof-detach-queue)) + (when (and (boundp 'prover-was-busy) + (or proc-killed was-busy)) + (setq prover-was-busy t)))) (defun coq-par-process-filter (process output) "Store output from coq background compilation." -- cgit v1.2.3 From 4bcac92df46da9e68b5e3d565bb118fb63b4feb4 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 19 Jan 2017 11:40:28 +0100 Subject: save settings not defined with defpacustom (fixes #142) - infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual --- coq/coq-abbrev.el | 90 ++++++++++++++++++++++++++++++++--------------- coq/coq-compile-common.el | 21 ++++++++--- coq/coq.el | 6 ++++ 3 files changed, 85 insertions(+), 32 deletions(-) (limited to 'coq') diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 534c013d..2b318dea 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -169,34 +169,68 @@ It was constructed with `proof-defstringset-fn'.") coq-compile-parallel-in-background) :help ,(concat "Continue background compilation after " "the first error as far as possible")] - ["no quick" - (customize-set-variable 'coq-compile-quick 'no-quick) - :style radio - :selected (eq coq-compile-quick 'no-quick) - :active (and coq-compile-before-require - coq-compile-parallel-in-background) - :help "Compile without -quick but accept existion .vio's"] - ["quick no vio2vo" - (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo) - :style radio - :selected (eq coq-compile-quick 'quick-no-vio2vo) - :active (and coq-compile-before-require - coq-compile-parallel-in-background) - :help "Compile with -quick, accept existing .vo's, don't run vio2vo"] - ["quick and vio2vo" - (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo) - :style radio - :selected (eq coq-compile-quick 'quick-and-vio2vo) - :active (and coq-compile-before-require - coq-compile-parallel-in-background) - :help "Compile with -quick, accept existing .vo's, run vio2vo later"] - ["ensure vo" - (customize-set-variable 'coq-compile-quick 'ensure-vo) - :style radio - :selected (eq coq-compile-quick 'ensure-vo) - :active (and coq-compile-before-require - coq-compile-parallel-in-background) - :help "Ensure only vo's are used for consistency"] + ("Quick compilation" + ["no quick" + (customize-set-variable 'coq-compile-quick 'no-quick) + :style radio + :selected (eq coq-compile-quick 'no-quick) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Compile without -quick but accept existion .vio's"] + ["quick no vio2vo" + (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo) + :style radio + :selected (eq coq-compile-quick 'quick-no-vio2vo) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Compile with -quick, accept existing .vo's, don't run vio2vo"] + ["quick and vio2vo" + (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo) + :style radio + :selected (eq coq-compile-quick 'quick-and-vio2vo) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Compile with -quick, accept existing .vo's, run vio2vo later"] + ["ensure vo" + (customize-set-variable 'coq-compile-quick 'ensure-vo) + :style radio + :selected (eq coq-compile-quick 'ensure-vo) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Ensure only vo's are used for consistency"] + ) + ("Auto Save" + ["Query coq buffers" + (customize-set-variable 'coq-compile-auto-save 'ask-coq) + :style radio + :selected (eq coq-compile-auto-save 'ask-coq) + :active coq-compile-before-require + :help "Ask for each coq-mode buffer, except the current buffer"] + ["Query all buffers" + (customize-set-variable 'coq-compile-auto-save 'ask-all) + :style radio + :selected (eq coq-compile-auto-save 'ask-all) + :active coq-compile-before-require + :help "Ask for all buffers"] + ["Autosave coq buffers" + (customize-set-variable 'coq-compile-auto-save 'save-coq) + :style radio + :selected (eq coq-compile-auto-save 'save-coq) + :active coq-compile-before-require + :help "Save all Coq buffers without confirmation, except the current one"] + ["Autosave all buffers" + (customize-set-variable 'coq-compile-auto-save 'save-all) + :style radio + :selected (eq coq-compile-auto-save 'save-all) + :active coq-compile-before-require + :help "Save all buffers without confirmation"] + ) + ["Lock Ancesotors" + coq-lock-ancestors-toggle + :style toggle + :selected coq-lock-ancestors + :active coq-compile-before-require + :help "Lock files of imported modules"] ["Confirm External Compilation" coq-confirm-external-compilation-toggle :style toggle diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 4b0033d1..72a16881 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -246,7 +246,10 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes ensure-vo Ensure that all library dependencies are present as .vo files and delete outdated .vio files or .vio files that are more recent than the corresponding .vo file. This - setting is the only one that ensures soundness." + setting is the only one that ensures soundness. + +This option can be set via menu +`Coq -> Auto Compilation -> Quick compilation'." :type '(radio (const :tag "don't use -quick but accept existing vio files" no-quick) @@ -371,7 +374,10 @@ This makes four permitted values: 'ask-coq to confirm saving all modified Coq buffers, 'ask-all to confirm saving all modified buffers, 'save-coq to save all modified Coq buffers without confirmation and 'save-all to save all modified buffers without -confirmation." +confirmation. + +This option can be set via menu +`Coq -> Auto Compilation -> Auto Save'." :type '(radio (const :tag "ask for each coq-mode buffer, except the current buffer" @@ -389,17 +395,24 @@ confirmation." "If non-nil, lock ancestor module files. If external compilation is used (via `coq-compile-command') then only the direct ancestors are locked. Otherwise all ancestors are -locked when the \"Require\" command is processed." +locked when the \"Require\" command is processed. + +This option can be set via menu +`Coq -> Auto Compilation -> Lock Ancestors'." + :type 'boolean :safe 'booleanp :group 'coq-auto-compile) +;; define coq-lock-ancestors-toggle +(proof-deftoggle coq-lock-ancestors) + (defpacustom confirm-external-compilation t "If set let user change and confirm the compilation command. Otherwise start the external compilation without confirmation. This option can be set/reset via menu -`Coq -> Settings -> Confirm External Compilation'." +`Coq -> Auto Compilation -> Confirm External Compilation'." :type 'boolean :group 'coq-auto-compile) diff --git a/coq/coq.el b/coq/coq.el index edf905ae..f6c67475 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1544,6 +1544,12 @@ Near here means PT is either inside or just aside of a comment." ;; FIXME da: Does Coq have a help or about command? ;; proof-info-command "Help" + ;; Settings not defined with defpacustom because they have an unsupported + ;; type. + (setq proof-assistant-additional-settings + '(coq-compile-quick coq-compile-keep-going + coq-compile-auto-save coq-lock-ancestors)) + (setq proof-goal-command-p 'coq-goal-command-p proof-find-and-forget-fn 'coq-find-and-forget pg-topterm-goalhyplit-fn 'coq-goal-hyp -- cgit v1.2.3