diff options
| author | Matthieu Sozeau | 2016-03-16 18:00:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-03-16 18:05:42 +0100 |
| commit | bfce815bd1fa2c603141661b209a864c67ae1dbf (patch) | |
| tree | 64d2897047a845274845b4b3ffc585602841514c /dev/include | |
| parent | 34c467a4e41e20a9bf1318d47fbc09da94c5ad97 (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 'dev/include')
0 files changed, 0 insertions, 0 deletions
