diff options
| -rw-r--r-- | coq/coq-db.el | 4 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 1 |
2 files changed, 4 insertions, 1 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index 9c472f91..b29c8c57 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -157,12 +157,14 @@ for DB structure." " ... " (car-safe (car-safe (nthcdr (- size 1) db))))) +(defun coq-sort-menu-entries (menu) + (sort menu '(lambda (x y) (string< (downcase (elt x 0)) (downcase (elt y 0)))))) (defun coq-build-menu-from-db (db &optional size) "Take a keyword database DB and return a list of insertion menus for them. Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB structure." - (let* ((l db) (res + (let* ((l (coq-sort-menu-entries db)) (res ()) (wdth (+ 2 (max-length-db coq-tactics-db))) (sz (or size 30)) (lgth (length l))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 8e84b18d..5bdb08d0 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -451,6 +451,7 @@ so for the following reasons: ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") + ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") ("Import" nil "Import #." t "Import") ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") ("Inspect" nil "Inspect #." nil "Inspect") |