aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorHugo Herbelin2014-09-10 10:18:24 +0200
committerHugo Herbelin2014-09-10 10:58:06 +0200
commit5350d21315f6c6347c0b44e510ed8b8805cc2119 (patch)
treeb04c2d460d5a21e47bc0843a6244a1a989c54926 /kernel/nativelambda.ml
parentb3a5450370b64ef59bd08f9ac2dc3862b9a37e6c (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/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions