aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-30 22:43:12 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-30 22:43:12 +0000
commite586481eb0a73af7d3639d4f31acf3c71f67f45f (patch)
tree7646725db81d78042aeca2b34fb3df8ce3f6f5ce /coq/coq-syntax.el
parent19c50038d90be840be9f99ddee4fd51c1098c045 (diff)
Fix syntax for Local prefix (see Trac #348)
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r--coq/coq-syntax.el8
1 files changed, 4 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index b918a9a8..7e7614da 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -488,7 +488,7 @@ See also `coq-prog-env' to adjust the environment."
("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure")
("Cd" nil "Cd #." nil "Cd")
("Check" nil "Check" nil "Check")
- ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope")
+ ("Local Close Scope" "lclsc" "Local Close Scope #" t "Local\\s-+Close\\s-+Scope")
("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope")
("Comments" nil "Comments #." nil "Comments")
("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" )
@@ -519,13 +519,13 @@ See also `coq-prog-env' to adjust the environment."
("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t)
("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t)
("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t)
- ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t)
- ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local")
+ ("Local Notation (only parsing)" "lnotsp" "Local Notation # := # (only parsing)." t)
+ ("Local Notation" "lnots" "Local Notation # := #." t "Local\\s-+Notation")
("Notation (simple)" "nots" "Notation # := #." t "Notation")
("Typeclasses Opaque" nil "Typeclasses Opaque #." nil "Typeclasses\\s-+Opaque")
("Opaque" nil "Opaque #." nil "Opaque")
("Obligation Tactic" nil "Obligation Tactic := #." t "Obligation\\s-+Tactic")
- ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope")
+ ("Local Open Scope" "lopsc" "Local Open Scope #" t "Local\\s-+Open\\s-+Scope")
("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope")
("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions")
("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint)