branch: elpa/proof-general
commit 99f91e873ec2fdc41079555db1130f07d9a9ce89
Author: Erik Martin-Dorel <erik.martin-do...@irit.fr>
Commit: GitHub <nore...@github.com>
fix(coq.el): (setq proof-shell-strip-crs-from-input nil) (#774)
Related: https://github.com/ProofGeneral/PG/issues/773
---
coq/coq.el | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/coq/coq.el b/coq/coq.el
index fdafe2dd43..28d1be2887 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1988,6 +1988,10 @@ at `proof-assistant-settings-cmds' evaluation time.")
proof-shell-interrupt-regexp coq-interrupt-regexp
proof-shell-assumption-regexp coq-id
proof-shell-theorem-dependency-list-regexp
coq-shell-theorem-dependency-list-regexp
+ ;; CRs now can and should be preserved (to support String-related theories),
+ ;; see also this GitHub issue: https://github.com/ProofGeneral/PG/issues/773
+ proof-shell-strip-crs-from-input nil
+
pg-subterm-first-special-char ?\360
;; The next three represent path annotation information
pg-subterm-start-char ?\372 ; not done
