aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2006-12-22 17:53:21 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2006-12-22 17:53:21 +0000
commit57db4d603f3ea66794278a39fa7eacdc6aed9b02 (patch)
treeef2db1aecd2dfbaf33f6f4e7ef95b52468d8ac13 /coq/coq-syntax.el
parent84e2c1e93d5b55f3746c0ddd408dab13134a9b2d (diff)
Added some keywords ("Declare Module Import"...).
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r--coq/coq-syntax.el8
1 files changed, 8 insertions, 0 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index d9cd479d..f20b7ad5 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -313,6 +313,10 @@ so for the following reasons:
("Coinductive" "coindv" "Coinductive # : # :=\n|# : #." t "Coinductive")
("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module")
("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful
+ ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t "Declare\\s-+Module")
+ ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful
+ ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t "Declare\\s-+Module")
+ ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful
("Definition" "def" "Definition #:# := #." t "Definition");; careful
("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t)
("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t)
@@ -335,6 +339,10 @@ so for the following reasons:
("Ltac" "ltac" "Ltac # := #" t "Ltac")
("Module :=" "mo" "Module # : # := #." t ) ; careful
("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful
+ ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful
+ ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful
+ ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful
+ ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful
("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record")
("Scheme" "sc" "Scheme @{name} := #." t "Scheme")
("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t)