From 8a590a18d267424809c9bbea5017e0d9e993c663 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 5 Feb 2013 16:47:04 +0000 Subject: Revert "Ordered evars by level of dependency in the merging phase of unification" Though this commit provides with more "natural" instances of metas found by unification, it breaks a few contribs. The best approach to try is maybe now to instead plug apply on evarconv.ml, rather than on unification.ml! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16191 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/unification.ml | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3a67a13ab..d5fee4595 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -827,14 +827,6 @@ let order_metas metas = meta :: order latemetas metas in order [] metas -(* Give priority to the less-dependent evars so that instances found - by matching are preferred over instances found by unification of - types of other instances; this gives instances more faithful to - what the user sees *) - -let order_evars evars = - Sort.list (fun (env1,(evk1,_),rhs1) (env2,(evk2,_),rhs2) -> evk1 < evk2) evars - (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn ts env evd ev rhs = @@ -943,7 +935,7 @@ let w_merge env with_types flags (evd,metas,evars) = else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in (* merge constraints *) - w_merge_rec evd (order_metas metas) (order_evars evars) [] + w_merge_rec evd (order_metas metas) evars [] let w_unify_meta_types env ?(flags=default_unify_flags) evd = let metas,evd = retract_coercible_metas evd in -- cgit v1.2.3