aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r--coq/coq-syntax.el1
1 files changed, 1 insertions, 0 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 7060f2d0..1540c467 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -373,6 +373,7 @@ so for the following reasons:
("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful
("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful
("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record")
+ ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure")
("Scheme" "sc" "Scheme @{name} := #." t "Scheme")
("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t)
("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t)