From d8b501a5caf50ede62631e3fa30aa89f53db045f Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sat, 4 May 2019 01:28:57 +0200
Subject: proof-syntax.el: Fix an out-of-range bug in function `proof-format'

This bug seems to date from the generalization performed in commit:
080babbb0f361885e9b502ee56dec14351104a37
---
 generic/proof-syntax.el | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index cdc38775..6fbe8eb0 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -244,15 +244,17 @@ may be a string or sexp evaluated to get a string."
   (while alist
     (let ((idx 0))
       (while (string-match (car (car alist)) string idx)
-	(setq string
-	      (concat (substring string 0 (match-beginning 0))
-		      (cond
-		       ((stringp (cdr (car alist)))
-			(cdr (car alist)))
-		       (t
-			(eval (cdr (car alist)))))
-		      (substring string (match-end 0))))
-	(setq idx (+ (match-beginning 0) (length (cdr (car alist)))))))
+	(let ((replacement
+	       (cond
+		((stringp (cdr (car alist)))
+		 (cdr (car alist)))
+		(t
+		 (eval (cdr (car alist)))))))
+	  (setq string
+		(concat (substring string 0 (match-beginning 0))
+			replacement
+			(substring string (match-end 0))))
+	  (setq idx (+ (match-beginning 0) (length replacement))))))
     (setq alist (cdr alist)))
   string)
 
-- 
cgit v1.2.3