From f2a148db80fb52e9adf8ddd3f4c8e6695056d131 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 15 Mar 2004 17:13:08 +0000
Subject: bug fix in holes (call to proof-indent-line instead of funcall
 indent-line-function).

---
 generic/holes.el        | 2 +-
 generic/proof-config.el | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/holes.el b/generic/holes.el
index cd559eb2..4d7fe7b0 100644
--- a/generic/holes.el
+++ b/generic/holes.el
@@ -794,7 +794,7 @@ end of last abbrev expansion. "
 	 (save-excursion 
 		(previous-line n)
 		(while (>= n 0)
-		  (proof-indent-line)
+		  (funcall indent-line-function)
 		  (next-line 1)
 		  (setq n (- n 1))
 		  )
diff --git a/generic/proof-config.el b/generic/proof-config.el
index cd1b0413..fb17dc4e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1164,6 +1164,8 @@ proof-goal-command-regexp instead)."
 ;;  move the code of isar-global-save-command-p to proof-done-advancing.
 ;; FIXME da: sounds like a good idea, then that would give us a proper 
 ;;  handling of nested proofs?
+;; FIXME: Pierre:Careful: in coq V8 I now need a function to detect save 
+;;  command. Because Proof <term>. is a term, but not Proof with ...
 ;;
 (defcustom proof-really-save-command-p (lambda (span cmd) t)
   "Is this really a save command?
-- 
cgit v1.2.3