coq-unicode-tokens
Table of Contents
- Emacs package
- Proof General
Feature that provides Coq-specific proof-unicode-tokens support.
1. usage
The main configuration variables are coq-token-symbol-map and coq-shortcut-alist.
As of , these variables use coq-unicode-tokens-set as a setter, so they need to be set via setopt (or some such).
2. defaults
The default configuration is rather confusing. As of :
In other words, by default, it both displays Unicode tokens and also enables input shortcuts. Despite the recommendation, this seems unintuitive to me: you probably want just one mode, not both.