From 36ca763e45d4b4489983cd820b28a5d36cea04de Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 8 Mar 2005 17:08:28 +0000
Subject: small modifications, updating doc string of holes.el.

---
 coq/coq-abbrev.el | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 29fc9b96..c73b4e4d 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -195,14 +195,14 @@
       )
      ("Notations"
       "COMMAND               ABBREVIATION"
-      ["Infix                           inf<C-BS>" (holes-insert-and-expand "inf") t]     
-      ["Notation (no assoc)             nota<C-BS>" (holes-insert-and-expand "nota") t]     
-      ["Notation (assoc)                notas<C-BS>" (holes-insert-and-expand "notas") t]     
-      ["Notation (no assoc, scope)      notasc<C-BS>" (holes-insert-and-expand "notasc") t]     
-      ["Notation (assoc, scope)         notassc<C-BS>" (holes-insert-and-expand "notassc") t]
-		""
-      ["Notation (simple)               nots<C-BS>" (holes-insert-and-expand "nots") t]     
-      ["Notation (simple,local)         notsl<C-BS>" (holes-insert-and-expand "nots") t]     
+      ["Infix                      inf<C-BS>" (holes-insert-and-expand "inf") t]     
+      ["Notation (no assoc)        nota<C-BS>" (holes-insert-and-expand "nota") t]     
+      ["Notation (assoc)           notas<C-BS>" (holes-insert-and-expand "notas") t] 
+      ["Notation (no assoc, scope) notasc<C-BS>" (holes-insert-and-expand "notasc") t] 
+      ["Notation (assoc, scope)    notassc<C-BS>" (holes-insert-and-expand "notassc") t]
+      ""
+      ["Notation (simple)          nots<C-BS>" (holes-insert-and-expand "nots") t]     
+      ["Notation (simple,local)    notsl<C-BS>" (holes-insert-and-expand "nots") t]     
 
       )
      )
-- 
cgit v1.2.3