Commit 8c7e9ad
committed
reduce projs
When encountering a projection, we weak-head reduce its subject. If we obtain a
constructor, we reduce the projection immediately (without backtracking).
Otherwise and if the reduced subject is not ground, we try solving the
canonical structure problem after refolding the other term to its state
at the start of the unification.1 parent 9ce8eb3 commit 8c7e9ad
File tree
3 files changed
+173
-180
lines changed- pretyping
- test-suite/bugs
3 files changed
+173
-180
lines changed
0 commit comments