Removed an evar_merge in clenv_fchain which not only is incorrect but

is an important cause of inefficiency when the number of evars is large.

It is wrong in the sense that it assumes the two sigma given to
clenv_fchain to be disjoint. This is true for metas, but not for
evars. It used to be useful in some respect when clenv bindings were
represented by open_constr, each of them having private evars (see
r10151 which introduced this evar_merge), but determining what evars
were private which and were shared is hopeless. Since the removal of
private sigmas in r12603, evars in clenv bindings are assumed to be
extended monotonically and clenv_fchain should only have to take the
most recent evars - assumed to be the first argument - instead of a
union.

The function clenv_fchain remains anyway fragile since it is
asymmetric. More should be done to clean it up so that it receives
only one - unambiguous - evars argument, what would mean actually,
receiving only one clausenv and the second argument being just a
template pair (t:T).

The call to evar_merge was source of inefficiency. On some calls to
omega in contrib JordanCurveTheorem, removing it reduces the execution
time by a factor larger than 5 (from 400s down to 70s on my Core 2 Duo).

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

1 files changed, 1 insertions, 2 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 006892189..48d78d858 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -344,8 +344,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv
   let clenv' =
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
-      evd =
-        evar_merge (meta_merge clenv.evd nextclenv.evd) clenv.evd;
+      evd = meta_merge nextclenv.evd clenv.evd;
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =