diff options
| author | Théo Zimmermann | 2019-03-12 21:48:04 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-12 21:48:04 +0100 |
| commit | a249cc95c1345442c67e240e881fb653579ee386 (patch) | |
| tree | 9ac27e3b3964bcf2434148740ba2b32ab09c6c16 /plugins/syntax/string_notation.mli | |
| parent | f1d60cad76439d96da36ed7c52ff71b1b9573b80 (diff) | |
[refman] Add 'warn' option to coqtop directive.
Fix semantic conflict between #9389 and #9654.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions