diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-30 17:38:29 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-30 17:38:29 +0000 |
| commit | 0373800479dfeefbe6dabccaa476c42a368f6d46 (patch) | |
| tree | 7f532726b6acd17b7193fa105de3169e46760baa /pretyping/unification.ml | |
| parent | eab82e1f4d3c43c894383d54bbfcf9eea112de94 (diff) | |
Speed-up refine by avoiding some calls to Evd.fold
Instead of the full Evd.fold, Evd.fold_undefined seems enough in
- Evarutil.push_dependent_evars
- the nf_evars call in Evarutil.evars_to_metas
(we hence create a function nf_evars_undefined and use it there)
This should bring back Compcert into reasonable compilation time
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
0 files changed, 0 insertions, 0 deletions