diff options
| author | Pierre Courtieu | 2000-08-26 11:05:07 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2000-08-26 11:05:07 +0000 |
| commit | 8eb18e285ae9c8e64b3bc6193ff050c858117855 (patch) | |
| tree | bc66f0a5d6170eb3dae0470bcc5595a72aad0a30 /coq/x-symbol-coq.el | |
| parent | 76e90b9e529118677ce70df3d92339a66992c346 (diff) | |
Some changes for undoing with coq, handle user-defined tactics, in
coq/coq-syntax.el and coq/coq.el.
Diffstat (limited to 'coq/x-symbol-coq.el')
| -rw-r--r-- | coq/x-symbol-coq.el | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el index 3f77c1b3..7c09b2ef 100644 --- a/coq/x-symbol-coq.el +++ b/coq/x-symbol-coq.el @@ -6,7 +6,9 @@ ;; (defvar x-symbol-coq-symbol-table - '((perpendicular () "False" "\\<bottom>") + '((arrowup () "\\+" "\\<uparrow>") + (arrowdown () "\\-" "\\<downarrow>") + (perpendicular () "False" "\\<bottom>") (top () "True" "\\<top>") (notsign () "~" "\\<not>") (longarrowright () "->" "\\<longrightarrow>") @@ -63,11 +65,11 @@ (defvar x-symbol-coq-case-insensitive nil) ;Pierre: let's try this, phi1 will be encoded, but not phia or -;philosophy. problem: blaphi will be encoded, other problem: false1 -;sholud not be encoded (this on eshould be easy: -;x-symbol-coq-token-shape is a list) +;philosophy. problem: blaphi will be encoded, +; other problem: false1 sholud not be encoded + +(defvar x-symbol-coq-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]")) -(defvar x-symbol-coq-token-shape '(?_ "[A-Za-z]+" . "[^0-9\ \t\n]")) ;(defvar x-symbol-coq-token-shape nil) (defvar x-symbol-coq-table x-symbol-coq-symbol-table) |