From 60dcd96a3efaff3cde5d11873ff82669d8dbe993 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 8 Mar 2016 16:03:24 +0100
Subject: Fixing #62.

I don't know if it is a coq bug that bullet do not support Time. I
remove Time from bullets for the moment.
---
 coq/coq.el | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index 40af5aa2..bde53667 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1904,12 +1904,16 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 (defconst coq--time-prefix "Time "
   "Coq command prefix for displaying timing information.")
 
+(defun coq-bullet-p (s)
+  (string-match coq-bullet-regexp-nospace s))
+
 ;; Remark: `action' and `string' are known by `proof-shell-insert-hook'
 (defun coq-preprocessing ()
   (when coq-time-commands
     (with-no-warnings  ;; NB: dynamic scoping of `string' and `action'
       ;; Don't add the prefix if this is a command sent internally
-      (unless (eq action 'proof-done-invisible)
+      (unless (or (eq action 'proof-done-invisible)
+                  (coq-bullet-p string)) ;; coq does not accept "Time -".
         (setq string (concat coq--time-prefix string))))))
 
 (add-hook 'proof-shell-insert-hook 'coq-preprocessing)
-- 
cgit v1.2.3