From 11b03d47628bf833e98e0b3d8ae9c5c9a358235d Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sun, 28 Feb 2016 19:20:11 -0500
Subject: Don't add the ‘Time’ prefix to internal Coq commands

This ensures that parts of Proof General that use Coq commands in the
background are not confused by extra timing information.
---
 coq/coq.el | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 9e4621aa..9c255260 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1906,9 +1906,11 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 
 ;; Remark: `action' and `string' are known by `proof-shell-insert-hook'
 (defun coq-preprocessing ()
-  (if coq-time-commands
+  (when coq-time-commands
+    ;; Don't add the prefix if this is a command sent internally
+    (unless (memq 'no-response-display proof-shell-delayed-output-flags)
       (with-no-warnings  ;; NB: dynamic scoping of `string'
-        (setq string (concat coq--time-prefix string)))))
+        (setq string (concat coq--time-prefix string))))))
 
 (add-hook 'proof-shell-insert-hook 'coq-preprocessing)
 
-- 
cgit v1.2.3