aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-03-16 18:00:25 +0100
committerMatthieu Sozeau2016-03-16 18:05:42 +0100
commitbfce815bd1fa2c603141661b209a864c67ae1dbf (patch)
tree64d2897047a845274845b4b3ffc585602841514c /kernel/nativecode.mli
parent34c467a4e41e20a9bf1318d47fbc09da94c5ad97 (diff)
Fix incorrect behavior of CS resolution
Due to a change in pretyping, using cast annotations as typing constraints, the canonical structure problems given to the unification could contain non-evar-normalized terms, hence we force evar normalization where necessary to ensure the same CS solutions can be found. Here the dependency test is fooled by an erasable dependency, and the following resolution needs a independent codomain for pop b to be well-scoped.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions