Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.

Fix a few more cl.el leftovers.  Get rid of remaining use of iso-2022.
Use SMIE unconditionally.

* coq/coq-abbrev.el: Use lexical-binding.
(coq-install-abbrevs): Delete, only keep the relevant contents.
(proof-defstringset-fn): Remove.  Fold changes into the main version.

* coq/coq-indent.el (coq-find-real-start): Use forward-comment.

* coq/coq-smie.el: Use lexical-binding.  Assume `smie` is available.
(coq--string-suffix-p): Rename from coq-string-suffix-p.
Use string-suffix-p for it when available.
(string-suffix-p): Never define here.  Change all users to use
coq--string-suffix-p instead.
(coq-smie-.-deambiguate): Use forward-comment.  Remove unused var `beg`.
(coq-backward-token-fast-nogluing-dot-friends)
(coq-forward-token-fast-nogluing-dot-friends): Remove unused var
`tok-other`.
(coq-smie-search-token-backward): Remove unused var `p`.
(coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before
over looking-back.
(coq-smie-rules): Use `pcase` over deprecated cl's `case`.

* coq/coq-syntax.el: Use lexical-binding.
(coq-count-match): Rewrite so it doesn't do needless heap-allocation.
(coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p):
Use case-fold-search rather than proof-string-match.
(coq-goal-command-regexp): Forward-declare.
(coq-save-command-regexp-strict): Move before first use.
(coq-reserved-regexp): Use a single \_< ... \_>.
(coq-detect-hyps-positions): Limit search for looking-back.

* coq/coq.el: Remove SMIE declarations since SMIE is always used.
(coq-use-smie): Remove, unused.
(coq-smie): Always require.

* generic/pg-pbrpm.el: Fix leftover cl.el uses.

* generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error
in the docstring, improve interactive prompt.

* lib/maths-menu.el: Use utf-8 and lexical-binding.

1 files changed, 251 insertions, 251 deletions

diff --git a/lib/maths-menu.el b/lib/maths-menu.el
index 32911a35..43592bed 100644
--- a/lib/maths-menu.el
+++ b/lib/maths-menu.el
@@ -1,13 +1,13 @@
-;;; maths-menu.el --- insert maths characters from a menu  -*-coding: iso-2022-7bit;-*-
+;;; maths-menu.el --- insert maths characters from a menu  -*- lexical-binding:t; coding: utf-8 -*-
 
 ;; This file is part of Proof General.
 
-;; Portions ,A)(B Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions ,A)(B Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
-;; Portions ,A)(B Copyright 2001-2017  Pierre Courtieu
-;; Portions ,A)(B Copyright 2010, 2016  Erik Martin-Dorel
-;; Portions ,A)(B Copyright 2011-2013, 2016-2017  Hendrik Tews
-;; Portions ,A)(B Copyright 2015-2017  Cl,Ai(Bment Pit-Claudel
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017  Pierre Courtieu
+;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions © Copyright 2015-2017  Clément Pit-Claudel
 
 ;; Author: Dave Love <fx@gnu.org>
 ;; Keywords: convenience
@@ -86,262 +86,262 @@
 (defvar maths-menu-menu
   (maths-menu-build-menu
    '(("Logic"
-      (?$A!D(B "and")
-      (?$A!E(B "or")
-      (?$,1x (B "for all")
-      (?$,1x#(B "there exists")
-      (?$,1x$(B "there does not exist")
-      (?$,1yd(B "down tack")
-      (?$,1ye(B "up tack"))
+      (?∧ "and")
+      (?∨ "or")
+      (?∀ "for all")
+      (?∃ "there exists")
+      (?∄ "there does not exist")
+      (?⊤ "down tack")
+      (?⊥ "up tack"))
      ("Binops 1"
-      (?,A1(B "plus-minus sign")
-      (?$,1x3(B "minus-or-plus sign")
-      (?,AW(B "multiplication sign")
-      (?,Aw(B "division sign")
-      (?$,1x2(B "minus sign")
-      (?$,1x7(B "asterisk operator")
-      (?$,1z&(B "star operator")
-      (?$,2"+(B "white circle")
-      (?$,1s"(B "bullet")
-      (?,A7(B "middle dot")
-      (?$,1xI(B "intersection")
-      (?$,1xJ(B "union")
-      (?$,1yN(B "multiset union")
-      (?$,1yS(B "square cap")
-      (?$,1yT(B "square cup")
-      (?$,1xH(B "logical or")
-      (?$,1xG(B "logical and")
-      (?$,1x6(B "set minus")
-      (?$,1x`(B "wreath product"))
+      (?± "plus-minus sign")
+      (?∓ "minus-or-plus sign")
+      (?× "multiplication sign")
+      (?÷ "division sign")
+      (?− "minus sign")
+      (?∗ "asterisk operator")
+      (?⋆ "star operator")
+      (?○ "white circle")
+      (?• "bullet")
+      (?· "middle dot")
+      (?∩ "intersection")
+      (?∪ "union")
+      (?⊎ "multiset union")
+      (?⊓ "square cap")
+      (?⊔ "square cup")
+      (?∨ "logical or")
+      (?∧ "logical and")
+      (?∖ "set minus")
+      (?≀ "wreath product"))
      ("Binops 2"
-      (?$,1z$(B "diamond operator")
-      (?$,2!s(B "white up-pointing triangle")
-      (?$,2!}(B "white down-pointing triangle")
-      (?$,2"#(B "white left-pointing small triangle")
-      (?$,2!y(B "white right-pointing small triangle")
-      (?$,2"!(B "white left-pointing triangle")
-      (?$,2!w(B "white right-pointing triangle")
-      (?$,1yU(B "circled plus")
-      (?$,1yV(B "circled minus")
-      (?$,1yW(B "circled times")
-      (?$,1yX(B "circled division slash")
-      (?$,1yY(B "circled dot operator")
-      (?$,2"O(B "large circle")
-      (?$,1s (B "dagger")
-      (?$,1s!(B "double dagger")
-      (?$,1yt(B "normal subgroup of or equal to")
-      (?$,1yu(B "contains as normal subgroup or equal to"))
+      (?⋄ "diamond operator")
+      (?△ "white up-pointing triangle")
+      (?▽ "white down-pointing triangle")
+      (?◃ "white left-pointing small triangle")
+      (?▹ "white right-pointing small triangle")
+      (?◁ "white left-pointing triangle")
+      (?▷ "white right-pointing triangle")
+      (?⊕ "circled plus")
+      (?⊖ "circled minus")
+      (?⊗ "circled times")
+      (?⊘ "circled division slash")
+      (?⊙ "circled dot operator")
+      (?◯ "large circle")
+      (?† "dagger")
+      (?‡ "double dagger")
+      (?⊴ "normal subgroup of or equal to")
+      (?⊵ "contains as normal subgroup or equal to"))
      ("Relations 1"
-      (?$,1y$(B "less-than or equal to")
-      (?$,1y:(B "precedes")
-      (?$,1y*(B "much less-than")
-      (?$,1yB(B "subset of")
-      (?$,1yF(B "subset of or equal to")
-      (?$,1yO(B "square image of")
-      (?$,1yQ(B "square image of or equal to")
-      (?$,1x((B "element of")
-      (?$,1x)(B "not an element of")
-      (?$,1yb(B "right tack")
-      (?$,1y%(B "greater-than or equal to")
-      (?$,1y;(B "succeeds")
-      (?$,1y=(B "succeeds or equal to")
-      (?$,1y+(B "much greater-than")
-      (?$,1yC(B "superset of")
-      (?$,1yG(B "superset of or equal to")
-      (?$,1yP(B "square original of")
-      (?$,1yR(B "square original of or equal to")
-      (?$,1x+(B "contains as member")
-      (?$,1y!(B "identical to")
-      (?$,1y"(B "not identical to") )
+      (?≤ "less-than or equal to")
+      (?≺ "precedes")
+      (?≪ "much less-than")
+      (?⊂ "subset of")
+      (?⊆ "subset of or equal to")
+      (?⊏ "square image of")
+      (?⊑ "square image of or equal to")
+      (?∈ "element of")
+      (?∉ "not an element of")
+      (?⊢ "right tack")
+      (?≥ "greater-than or equal to")
+      (?≻ "succeeds")
+      (?≽ "succeeds or equal to")
+      (?≫ "much greater-than")
+      (?⊃ "superset of")
+      (?⊇ "superset of or equal to")
+      (?⊐ "square original of")
+      (?⊒ "square original of or equal to")
+      (?∋ "contains as member")
+      (?≡ "identical to")
+      (?≢ "not identical to") )
      ("Relations 2"
-      (?$,1yc(B "left tack")
-      (?$,1x\(B "tilde operator")
-      (?$,1xc(B "asymptotically equal to")
-      (?$,1xm(B "equivalent to")
-      (?$,1xh(B "almost equal to")
-      (?$,1xe(B "approximately equal to")
-      (?$,1y (B "not equal to")
-      (?$,1xp(B "approaches the limit")
-      (?$,1x=(B "proportional to")
-      (?$,1yg(B "models")
-      (?$,1xC(B "divides")
-      (?$,1xE(B "parallel to")
-      (?$,1z((B "bowtie")
-      (?$,1z((B "bowtie")
-      (?$,1{#(B "smile")
-      (?$,1{"(B "frown")
-      (?$,1xy(B "estimates")
-      (?$,1z_(B "z notation bag membership"))
+      (?⊣ "left tack")
+      (?∼ "tilde operator")
+      (?≃ "asymptotically equal to")
+      (?≍ "equivalent to")
+      (?≈ "almost equal to")
+      (?≅ "approximately equal to")
+      (?≠ "not equal to")
+      (?≐ "approaches the limit")
+      (?∝ "proportional to")
+      (?⊧ "models")
+      (?∣ "divides")
+      (?∥ "parallel to")
+      (?⋈ "bowtie")
+      (?⋈ "bowtie")
+      (?⌣ "smile")
+      (?⌢ "frown")
+      (?≙ "estimates")
+      (?⋿ "z notation bag membership"))
      ("Arrows"
-      (?$,1vp(B "leftwards arrow")
-      (?$,1wP(B "leftwards double arrow")
-      (?$,1vr(B "rightwards arrow")
-      (?$,1wR(B "rightwards double arrow")
-      (?$,1vt(B "left right arrow")
-      (?$,1wT(B "left right double arrow")
-      (?$,1w&(B "rightwards arrow from bar")
-      (?$,1w)(B "leftwards arrow with hook")
-      (?$,1w<(B "leftwards harpoon with barb upwards")
-      (?$,1w=(B "leftwards harpoon with barb downwards")
-      (?$,1wL(B "rightwards harpoon over leftwards harpoon")
-      (?$,1w&(B "rightwards arrow from bar")
-      (?$,1w*(B "rightwards arrow with hook")
-      (?$,1w@(B "rightwards harpoon with barb upwards")
-      (?$,1wA(B "rightwards harpoon with barb downwards")
-      (?$,1v}(B "rightwards wave arrow")
-      (?$,1vq(B "upwards arrow")
-      (?$,1wQ(B "upwards double arrow")
-      (?$,1vs(B "downwards arrow")
-      (?$,1wS(B "downwards double arrow")
-      (?$,1vu(B "up down arrow")
-      (?$,1vw(B "north east arrow")
-      (?$,1vx(B "south east arrow")
-      (?$,1vy(B "south west arrow")
-      (?$,1vv(B "north west arrow")
-      (?$,1w[(B "rightwards triple arrow"))
+      (?← "leftwards arrow")
+      (?⇐ "leftwards double arrow")
+      (?→ "rightwards arrow")
+      (?⇒ "rightwards double arrow")
+      (?↔ "left right arrow")
+      (?⇔ "left right double arrow")
+      (?↦ "rightwards arrow from bar")
+      (?↩ "leftwards arrow with hook")
+      (?↼ "leftwards harpoon with barb upwards")
+      (?↽ "leftwards harpoon with barb downwards")
+      (?⇌ "rightwards harpoon over leftwards harpoon")
+      (?↦ "rightwards arrow from bar")
+      (?↪ "rightwards arrow with hook")
+      (?⇀ "rightwards harpoon with barb upwards")
+      (?⇁ "rightwards harpoon with barb downwards")
+      (?↝ "rightwards wave arrow")
+      (?↑ "upwards arrow")
+      (?⇑ "upwards double arrow")
+      (?↓ "downwards arrow")
+      (?⇓ "downwards double arrow")
+      (?↕ "up down arrow")
+      (?↗ "north east arrow")
+      (?↘ "south east arrow")
+      (?↙ "south west arrow")
+      (?↖ "north west arrow")
+      (?⇛ "rightwards triple arrow"))
      ("Long arrows"
-      (?$,2'v(B "long rightwards arrow")
-      (?$,2'w(B "long left right arrow")
-      (?$,2'x(B "long left double arrow")
-      (?$,2'y(B "long right double arrow")
-      (?$,2'z(B "long left right double arrow")
-      (?$,2'{(B "long left arrow from bar")
-      (?$,2'|(B "long right arrow from bar")
-      (?$,2'}(B "long left double arrow bar")
-      (?$,2'~(B "long right double arrow from bar")
-      (?$,2'(B "long rightwards squiggle arrow"))
+      (?⟶ "long rightwards arrow")
+      (?⟷ "long left right arrow")
+      (?⟸ "long left double arrow")
+      (?⟹ "long right double arrow")
+      (?⟺ "long left right double arrow")
+      (?⟻ "long left arrow from bar")
+      (?⟼ "long right arrow from bar")
+      (?⟽ "long left double arrow bar")
+      (?⟾ "long right double arrow from bar")
+      (?⟿ "long rightwards squiggle arrow"))
      ("Symbols 1"
-      (?$,1uu(B "alef symbol") ; don't use letter alef (avoid bidi confusion)
-      (?$,1uO(B "planck constant over two pi")
-      (?$,1 Q(B "latin small letter dotless i")
-      (?$,1uS(B "script small l")
-      (?$,1uX(B "script capital p")
-      (?$,1u\(B "black-letter capital r")
-      (?$,1uQ(B "black-letter capital i")
-      (?$,1ug(B "inverted ohm sign")
-      (?$,1s2(B "prime")
-      (?$,1x%(B "empty set")
-      (?$,1x'(B "nabla")
-      (?$,1x:(B "square root")
-      (?$,1x;(B "cube root")
-      (?$,1x@(B "angle")
-      (?,A,(B "not sign")
-      (?$,2#o(B "music sharp sign")
-      (?$,1x"(B "partial differential")
-      (?$,1x>(B "infinity") )
+      (?ℵ "alef symbol") ; don't use letter alef (avoid bidi confusion)
+      (?ℏ "planck constant over two pi")
+      (?ı "latin small letter dotless i")
+      (?ℓ "script small l")
+      (?℘ "script capital p")
+      (?ℜ "black-letter capital r")
+      (?ℑ "black-letter capital i")
+      (?℧ "inverted ohm sign")
+      (?′ "prime")
+      (?∅ "empty set")
+      (?∇ "nabla")
+      (?√ "square root")
+      (?∛ "cube root")
+      (?∠ "angle")
+      (?¬ "not sign")
+      (?♯ "music sharp sign")
+      (?∂ "partial differential")
+      (?∞ "infinity") )
      ("Symbols 2"
-      (?$,2!a(B "white square")
-      (?$,2"'(B "white diamond")
-      (?$,2!u(B "white up-pointing small triangle")
-      (?$,1x1(B "n-ary summation")
-      (?$,1x/(B "n-ary product")
-      (?$,1x0(B "n-ary coproduct")
-      (?$,1xK(B "integral")
-      (?$,1xN(B "contour integral")
-      (?$,1z"(B "n-ary intersection")
-      (?$,1z#(B "n-ary union")
-      (?$,1z!(B "n-ary logical or")
-      (?$,1z (B "n-ary logical and")
-      (?$,1uU(B "double-struck capital n")
-      (?$,1uY(B "double-struck capital p")
-      (?$,1uZ(B "double-struck capital q")
-      (?$,1u](B "double-struck capital r")
-      (?$,1ud(B "double-struck capital z")
-      (?$,1uP(B "script capital i")
-      (?$,1![(B "latin small letter lambda with stroke")
-      (?$,1xT(B "therefore")
-      (?$,1s&(B "horizontal ellipsis")
-      (?$,1zO(B "midline horizontal ellipsis")
-      (?$,1zN(B "vertical ellipsis")
-      (?$,1zQ(B "down right diagonal ellipsis")
-      (?$,1zP(B "up right diagonal ellipsis")
-      (?$,2,!(B "z notation spot")
-      (?$,2,"(B "z notation type colon"))
+      (?□ "white square")
+      (?◇ "white diamond")
+      (?▵ "white up-pointing small triangle")
+      (?∑ "n-ary summation")
+      (?∏ "n-ary product")
+      (?∐ "n-ary coproduct")
+      (?∫ "integral")
+      (?∮ "contour integral")
+      (?⋂ "n-ary intersection")
+      (?⋃ "n-ary union")
+      (?⋁ "n-ary logical or")
+      (?⋀ "n-ary logical and")
+      (?ℕ "double-struck capital n")
+      (?ℙ "double-struck capital p")
+      (?ℚ "double-struck capital q")
+      (?ℝ "double-struck capital r")
+      (?ℤ "double-struck capital z")
+      (?ℐ "script capital i")
+      (?ƛ "latin small letter lambda with stroke")
+      (?∴ "therefore")
+      (?… "horizontal ellipsis")
+      (?⋯ "midline horizontal ellipsis")
+      (?⋮ "vertical ellipsis")
+      (?⋱ "down right diagonal ellipsis")
+      (?⋰ "up right diagonal ellipsis")
+      (?⦁ "z notation spot")
+      (?⦂ "z notation type colon"))
      ("Delimiters"
-      (?\$,1zj(B "left floor")
-      (?\$,1zh(B "left ceiling")
-      (?\$,1{)(B "left-pointing angle bracket")
-      (?\$,1zk(B "right floor")
-      (?\$,1zi(B "right ceiling")
-      (?\$,1{*(B "right-pointing angle bracket")
-      (?\$,2=Z(B "left white square bracket")
-      (?\$,2=[(B "right white square bracket")
-      (?\$,2=J(B "left double angle bracket")
-      (?\$,2=K(B "right double angle bracket")
-      (?\$,2,'(B "z notation left image bracket")
-      (?\$,2,((B "z notation right image bracket")
-      (?\$,2,)(B "z notation left binding bracket")
-      (?\$,2,*(B "z notation right binding bracket"))
+      (?\⌊ "left floor")
+      (?\⌈ "left ceiling")
+      (?\〈 "left-pointing angle bracket")
+      (?\⌋ "right floor")
+      (?\⌉ "right ceiling")
+      (?\〉 "right-pointing angle bracket")
+      (?\〚 "left white square bracket")
+      (?\〛 "right white square bracket")
+      (?\《 "left double angle bracket")
+      (?\》 "right double angle bracket")
+      (?\⦇ "z notation left image bracket")
+      (?\⦈ "z notation right image bracket")
+      (?\⦉ "z notation left binding bracket")
+      (?\⦊ "z notation right binding bracket"))
      ("Greek LC"
-      (?$,1'1(B "alpha")
-      (?$,1'2(B "beta")
-      (?$,1'3(B "gamma")
-      (?$,1'4(B "delta")
-      (?$,1'5(B "epsilon")
-      (?$,1'6(B "zeta")
-      (?$,1'7(B "eta")
-      (?$,1'8(B "theta")
-      (?$,1'Q(B "theta symbol")
-      (?$,1'9(B "iota")
-      (?$,1':(B "kappa")
-      (?$,1';(B "lamda")
-      (?$,1'<(B "mu")
-      (?$,1'=(B "nu")
-      (?$,1'>(B "xi")
-      (?$,1'@(B "pi")
-      (?$,1'V(B "pi symbol")
-      (?$,1'A(B "rho")
-      (?$,1'q(B "rho symbol")
-      (?$,1'C(B "sigma")
-      (?$,1'B(B "final sigma")
-      (?$,1'D(B "tau")
-      (?$,1'E(B "upsilon")
-      (?$,1'F(B "phi")
-      (?$,1'U(B "phi symbol")
-      (?$,1'G(B "chi")
-      (?$,1'H(B "psi")
-      (?$,1'I(B "omega"))
+      (?α "alpha")
+      (?β "beta")
+      (?γ "gamma")
+      (?δ "delta")
+      (?ε "epsilon")
+      (?ζ "zeta")
+      (?η "eta")
+      (?θ "theta")
+      (?ϑ "theta symbol")
+      (?ι "iota")
+      (?κ "kappa")
+      (?λ "lamda")
+      (?μ "mu")
+      (?ν "nu")
+      (?ξ "xi")
+      (?π "pi")
+      (?ϖ "pi symbol")
+      (?ρ "rho")
+      (?ϱ "rho symbol")
+      (?σ "sigma")
+      (?ς "final sigma")
+      (?τ "tau")
+      (?υ "upsilon")
+      (?φ "phi")
+      (?ϕ "phi symbol")
+      (?χ "chi")
+      (?ψ "psi")
+      (?ω "omega"))
      ("Greek UC"
-      (?$,1&s(B "Gamma")
-      (?$,1&t(B "Delta")
-      (?$,1&x(B "Theta")
-      (?$,1&{(B "Lamda")
-      (?$,1&~(B "Xi")
-      (?$,1' (B "Pi")
-      (?$,1'#(B "Sigma")
-      (?$,1'%(B "Upsilon")
-      (?$,1'&(B "Phi")
-      (?$,1'((B "Psi")
-      (?$,1')(B "Omega"))
+      (?Γ "Gamma")
+      (?Δ "Delta")
+      (?Θ "Theta")
+      (?Λ "Lamda")
+      (?Ξ "Xi")
+      (?Π "Pi")
+      (?Σ "Sigma")
+      (?Υ "Upsilon")
+      (?Φ "Phi")
+      (?Ψ "Psi")
+      (?Ω "Omega"))
      ("Sub/super"
-      (?$,1s}(B "superscript left parenthesis")
-      (?$,1s~(B "superscript right parenthesis")
-      (?$,1sz(B "superscript plus sign")
-      (?$,1s{(B "superscript minus")
-      (?$,1sp(B "superscript zero")
-      (?,A9(B "superscript one")
-      (?,A2(B "superscript two")
-      (?,A3(B "superscript three")
-      (?$,1st(B "superscript four")
-      (?$,1su(B "superscript five")
-      (?$,1sv(B "superscript six")
-      (?$,1sw(B "superscript seven")
-      (?$,1sx(B "superscript eight")
-      (?$,1sy(B "superscript nine")
-      (?$,1t-(B "subscript left parenthesis")
-      (?$,1t.(B "subscript right parenthesis")
-      (?$,1t*(B "subscript plus sign")
-      (?$,1t+(B "subscript minus")
-      (?$,1t (B "subscript zero")
-      (?$,1t!(B "subscript one")
-      (?$,1t"(B "subscript two")
-      (?$,1t#(B "subscript three")
-      (?$,1t$(B "subscript four")
-      (?$,1t%(B "subscript five")
-      (?$,1t&(B "subscript six")
-      (?$,1t'(B "subscript seven")
-      (?$,1t((B "subscript eight")
-      (?$,1t)(B "subscript nine")))))
+      (?⁽ "superscript left parenthesis")
+      (?⁾ "superscript right parenthesis")
+      (?⁺ "superscript plus sign")
+      (?⁻ "superscript minus")
+      (?⁰ "superscript zero")
+      (?¹ "superscript one")
+      (?² "superscript two")
+      (?³ "superscript three")
+      (?⁴ "superscript four")
+      (?⁵ "superscript five")
+      (?⁶ "superscript six")
+      (?⁷ "superscript seven")
+      (?⁸ "superscript eight")
+      (?⁹ "superscript nine")
+      (?₍ "subscript left parenthesis")
+      (?₎ "subscript right parenthesis")
+      (?₊ "subscript plus sign")
+      (?₋ "subscript minus")
+      (?₀ "subscript zero")
+      (?₁ "subscript one")
+      (?₂ "subscript two")
+      (?₃ "subscript three")
+      (?₄ "subscript four")
+      (?₅ "subscript five")
+      (?₆ "subscript six")
+      (?₇ "subscript seven")
+      (?₈ "subscript eight")
+      (?₉ "subscript nine")))))
 
 (defvar maths-menu-mode-map
   (let ((map (make-sparse-keymap)))