[ssr] avoid HO unif when doing truncation analysis

Eliminators can be:
- dependent: ... -> forall x (y : I x), P x y
- truncated: ... -> forall x (y : I x), P x
- funind like: ..-> forall x, P t
The user may provide a term t in `elim: t`
- t may be the last argument
- t may be the last "pattern" (standing for the last
argument of P)

We use unification to see if t (and its type) fits
in one of these cases (and/or to infer t).

This patch refuses to use unification in the HO case
eg `?T a = t` since the result is too often a false
positive.

0 files changed, 0 insertions, 0 deletions