diff options
| author | ppedrot | 2013-10-29 22:03:15 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-29 22:03:15 +0000 |
| commit | a35d9b2c4b374b9e5cbc6f302e4d3aac32dd0d78 (patch) | |
| tree | 3fac24fd8f2b19be34073b0abf83880bb5a55d36 | |
| parent | cfaae467fb84f8f7f63445b2efca23e8535e9a30 (diff) | |
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
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ff89553a21..9c21446da4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -970,7 +970,7 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd = types of metavars are unifiable with the types of their instances *) let head_app sigma m = - fst (decompose_appvect (whd_nored sigma m)) + fst (whd_nored_state sigma (m, empty_stack)) let check_types env flags (sigma,_,_ as subst) m n = if isEvar_or_Meta (head_app sigma m) then |