diff options
| author | Hugo Herbelin | 2014-09-10 10:18:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-10 10:58:06 +0200 |
| commit | 5350d21315f6c6347c0b44e510ed8b8805cc2119 (patch) | |
| tree | b04c2d460d5a21e47bc0843a6244a1a989c54926 /kernel/type_errors.ml | |
| parent | b3a5450370b64ef59bd08f9ac2dc3862b9a37e6c (diff) | |
Fixing inversion after having fixed intros_replacing
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations
when "as" is not given where equations coming from injection are not
yet removed, making invalid the computation of dependencies, what
prevents an hypothesis to be cleared and replaced.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions