From fd9544327956e2ac0ae6eff9845bc379f941de6f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 10 Sep 2009 22:31:13 +0000
Subject: proof-retract-until-point: protect against finding no span at all
 (mask current bug in Coq code)

---
 generic/proof-script.el | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index c6050abd..38feb34a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2222,7 +2222,11 @@ command."
 	  (proof-goto-end-of-locked)
 	  (backward-char)
 	  (setq span (span-at (point) 'type)))
-	(proof-retract-target span delete-region)))))
+	(if span 
+	  (proof-retract-target span delete-region)
+	  ;; something wrong
+	  (proof-debug 
+	   "proof-retract-until-point: couldn't find a span!"))))))
 
 
 
-- 
cgit v1.2.3