diff options
| author | Hugo Herbelin | 2018-10-23 15:59:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-23 16:46:35 +0200 |
| commit | c76fbecdfe4231ee3e0753c0efe665b1e8a8bba5 (patch) | |
| tree | 7f44f9a0a52125c7e8e12c8f28abd65140fbf4e2 /kernel/type_errors.ml | |
| parent | 10e908144df0c06f3ee182482470d7ac39a6cbc5 (diff) | |
Fixing #8794 (anomaly with abbreviation involving both term and binders).
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions