From defde678caf25e8a5110934d0f72d11897135f22 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 4 Feb 2003 12:23:03 +0000
Subject: Coq/pg: fixed a little bug with the "Print Hint" state preserving
 command, which must not be matched by the state changing command "Hint". I
 put "\\`Hint" in the keyword list, but I am not sure this is the best way.

---
 coq/coq-syntax.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 67407b14..006e20d1 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -186,7 +186,7 @@ Print and Check commands, put the following line in your .emacs:
     "Extraction\\s-+Language"
     "Extraction\\s-+NoInline"
     "Grammar"
-    "Hint" ;; not "Print Hint ." (proof-string-match coq-state-changing-commands-regexp "Hint toto")
+    "\\`Hint" ;; Pierre fev-2003: Hack: must not match "Print Hint."
     "Hints"
     "Identity\\s-+Coercion"
     "Implicit\\s-+Arguments\\s-+Off"
-- 
cgit v1.2.3