aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2005-11-28 12:49:05 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2005-11-28 12:49:05 +0000
commit43b9f5f09ad12b7235f0a61dcb8f4ec6559e9e59 (patch)
treec8e3cee297a9676695f4e7dceeed6bff7439ccab /coq
parent9daf902b767c7ea44db606f62e21142d2910f8c1 (diff)
added some keyword to coq tacics.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq-syntax.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 65e63b60..6ed5834f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -318,7 +318,8 @@ Print and Check commands, put the following line in your .emacs:
"Import"
"Infix"
"Load"
- "Notation"
+ "Notation"
+ "Open\\s-+Scope"
"Read\\s-+Module"
"Remove\\s-+LoadPath"
"Remove\\s-+Printing\\s-+If\\s-+ident"