From 99f91e873ec2fdc41079555db1130f07d9a9ce89 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Wed, 19 Jun 2024 14:09:59 +0200
Subject: [PATCH] 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 fdafe2dd4..28d1be288 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