From 8f0e60934c205b4fdba26c1e205988dca92bd02c Mon Sep 17 00:00:00 2001
From: Assia Mahboubi
Date: Fri, 7 Dec 2007 15:18:12 +0000
Subject: Print Coercions added to coq-syntax

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

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 1aa5c65d..33c4e6c3 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -532,6 +532,7 @@ so for the following reasons:
      ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic")
      ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope")
      ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope")
+     ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions")
      ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint)
      ("Print" "p" "Print #." nil "Print")
      ("Qed" nil "Qed." nil "Qed")
-- 
cgit v1.2.3