From 08170a5b4cc0a034654380b68c3280ab77081c1c Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Tue, 16 Mar 2004 16:16:13 +0000
Subject: Added one entry in the coq insert command menu (hint rewrite).

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

diff --git a/coq/coq.el b/coq/coq.el
index 867d8fd5..57c1836a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -119,6 +119,7 @@
      ["hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
      ["hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
      ["hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
+     ["hint Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
      ["hint extern           he<C-BS>" (insert-and-expand "he") t]
      ["hints                 hs<C-BS>" (insert-and-expand "hs") t]
      ""
-- 
cgit v1.2.3