diff options
| author | Maxime Dénès | 2017-05-23 09:12:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-23 09:12:02 +0200 |
| commit | 17e3f3b6a17145f7a51653de670263b7c3d613f3 (patch) | |
| tree | f8a08cae32c7636f2d00405d43581530f262e2e7 /pretyping/typeclasses_errors.ml | |
| parent | 3e5cbc1e5a18a21cd97c1077552314c84d59852e (diff) | |
| parent | 5b218f87bd59cfe9d510410c9acf78b5485391e1 (diff) | |
Merge PR#646: Revised behavior on ill-formed identifiers
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions