aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el1
1 files changed, 1 insertions, 0 deletions
diff --git a/coq/coq.el b/coq/coq.el
index bea485be..867d8fd5 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -758,6 +758,7 @@ This is specific to coq-mode."
proof-state-preserving-p 'coq-state-preserving-p)
(setq proof-save-command-regexp coq-save-command-regexp
+ proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>.
proof-save-with-hole-regexp coq-save-with-hole-regexp
proof-goal-with-hole-regexp coq-goal-with-hole-regexp
proof-nested-undo-regexp coq-state-changing-commands-regexp)