diff options
| author | Théo Zimmermann | 2018-11-30 21:35:12 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-03 13:59:33 +0100 |
| commit | 65d35e1294419e7f09903dace816750fd8d362eb (patch) | |
| tree | b6abe5486ff00ff19831f359f9ac0d4211e4e523 /pretyping/typeclasses_errors.ml | |
| parent | 0f0caf884d54fd81e0394dcedf0b77aaf8b19045 (diff) | |
Closes #9118: single backticks are made equivalent to double backticks; try to fix all misuses.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions