Do not rely on Reductionops to recognize canonical projections.

No need to call the whole whd_gen machinery when a simple matching over
a term would suffice.

Note that this changes a bit the semantics, but I suspect that the previous
code was buggy. Indeed, whd_nored also pushes cases and fixpoints on the
stack, so that an applied canonical projection inside such a context would
also match. But the caller in unification performs an approximate check where
the term needs to be an application or a projection, which would prevent
such complex situations most of the time, e.g. it would work with a dummy
commutative cut but not their corresponding vanilla match.

0 files changed, 0 insertions, 0 deletions