diff options
| author |  Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-16 13:51:43 +0000 |
|---|---|---|
| committer | Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-16 13:51:43 +0000 |
| commit | 6212b7f6c30ecae3bcd8d39a3332ed429c581b52 (patch) | |
| tree | a97b39d1562ffa1d097823252ebc8f5a67a15b07 /coq | |
| parent | 24ae82f9fc9816ca0a1e4de7447ce1db3a2baa28 (diff) | |
test commit : added Structure to coq-defn-db
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 1 |
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) |