diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-05-16 19:00:26 -0400 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-05-16 19:00:26 -0400 |
| commit | 3bcc3c41799dd8b8bf50d182346d962b67f396ab (patch) | |
| tree | 1d3c694348cbe46986ed41bbd3189e746e35d3d7 /coq/coq-syntax.el | |
| parent | 4346278e5ae54fe46a3dd04cb92892a0c9e045c0 (diff) | |
| parent | 9ae103b86dd3cdfc3e6e6326ebc1a8f803e50f7d (diff) | |
Merge branch 'master' of github.com:ProofGeneral/PG
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 94445439..fe996505 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1347,14 +1347,15 @@ It is used: (modify-syntax-entry ?< ".") (modify-syntax-entry ?> ".") (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?∀ "_") - (modify-syntax-entry ?∃ "_") - (modify-syntax-entry ?λ "_") ;; maybe a bad idea... lambda is a letter + (modify-syntax-entry ?_ "_") ; beware: word consituent EXCEPT in head position + (modify-syntax-entry ?\' "_") ; always word constituent + (modify-syntax-entry ?∀ ".") + (modify-syntax-entry ?∃ ".") + (modify-syntax-entry ?λ ".") ;; maybe a bad idea... lambda is a letter (modify-syntax-entry ?\| ".") ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug + ;; Hence the coq-with-altered-syntax-table below to put "." into "_" class temporarily (modify-syntax-entry ?\. ".") (modify-syntax-entry ?\* ". 23n") |