diff options
| author | Hugo Herbelin | 2015-10-19 16:06:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-19 16:08:17 +0200 |
| commit | c3967bd7a71df53a004478d23b072309f13f2ff5 (patch) | |
| tree | 4af71612aa02f318d1d7b1a7d0ba2738bdb7966b /kernel/type_errors.mli | |
| parent | 70d3ad33f6ba7a1c6b1fb93aadd5c05d7e9c03b8 (diff) | |
Turning anomaly into error for #4372 (weakness of inversion in the
presence of dependent types with only superficial dependency).
See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions