Commit c084cf7
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 780f301 commit c084cf7
File tree
3 files changed
+162
-181
lines changed- pretyping
- test-suite/bugs
3 files changed
+162
-181
lines changed
0 commit comments