diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-19 16:06:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-19 16:08:17 +0200 |
| commit | c3967bd7a71df53a004478d23b072309f13f2ff5 (patch) | |
| tree | 4af71612aa02f318d1d7b1a7d0ba2738bdb7966b /test-suite/bugs/closed/2141.v | |
| 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 'test-suite/bugs/closed/2141.v')
0 files changed, 0 insertions, 0 deletions