diff options
| author | Guillaume Melquiond | 2020-09-27 10:25:04 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-09-27 10:25:04 +0200 |
| commit | cb1a23c2fed25e395d4a6c17214cb5a005ae063a (patch) | |
| tree | cb3dd0bcaa768874ae7af031cab0f021356ea22f /plugins | |
| parent | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff) | |
Make "xxx:{{" always start a quotation, whether registered or not.
This commit also prevents quotations using "(" and "[" from gobbling
sentences. As a consequence, dynamically-registered quotations can no
longer modify where Coq sentences stop.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions