diff options
| author | Hugo Herbelin | 2018-10-31 00:12:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-31 11:22:56 +0100 |
| commit | 2a38552ad35cdcd827da014106aa5b4af88dfb9e (patch) | |
| tree | e415d01370fc0c53c8cc68ade2e01cf5ed13207a /kernel/type_errors.ml | |
| parent | 310f8fa900bc0d25a05f6409d941708a74aca60b (diff) | |
Notations: fixing a bug with abbreviations in custom entries.
Coercions were missing.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions