diff options
| author | Jasper Hugunin | 2019-05-03 23:22:56 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2019-05-03 23:22:56 -0700 |
| commit | 62b19246a81adbd07992cca91009faf012c5e9dd (patch) | |
| tree | 6eb12d5ec104e777cdcace6c7ed8f7bdc0d9fdd1 /kernel/type_errors.mli | |
| parent | 6960da4736186fa6214854329f36f558e7aa4d0b (diff) | |
CoqIDE: recognize qualified identifiers as words.
Fixes coq/coq#10062.
The implementation is rough, and does not deal with leading,
trailing, or doubled periods, but the same can be said of the current
handling of leading numbers or primes.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions