Optimized dependencies for pattern-matching on only trivial patterns.

If a term is matched only against variables, it will not introduce a
"match" and thus, even if the term is of an inductive type, its
indices will not be taken into account in the current algorithm
(though one could imagine an algorithm which does an expansion
specially in order to filter on indices).

This allows to tell the unification not to use dependencies which the
pattern-matching algorithm is not able to exploit in practice.

See example in file 2733.v.

0 files changed, 0 insertions, 0 deletions