Optimization in unification: when checking that the head of a term is an

evar or a meta, don't reconstruct the whole term. This hopefully saves
a lot of useless allocations and computing time.

I may have slightly changed the heuristic though, as only evars in front of
applications where recognized as such, whereas now this pass through cases
and fixpoints. I am walking on thin ice, but the test-suite was OK...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16956 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions