diff options
| author | herbelin | 2013-01-27 14:36:39 +0000 |
|---|---|---|
| committer | herbelin | 2013-01-27 14:36:39 +0000 |
| commit | 8d77cb907a3595c90f15e1aa6402868ad4e43242 (patch) | |
| tree | c5bf1e3aa9ee27fd47fa766e8c540f976e809ad5 | |
| parent | 68b1fa3bceffef3c3dfef8b2f041f2e5eb4d3173 (diff) | |
Ordered evars by level of dependency in the merging phase of unification
so as to get instances of evars closer from what the user sees.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16160 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6f7e2ba6f1..87025b4d22 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -827,6 +827,14 @@ 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 = @@ -935,7 +943,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) evars [] + w_merge_rec evd (order_metas metas) (order_evars evars) [] let w_unify_meta_types env ?(flags=default_unify_flags) evd = let metas,evd = retract_coercible_metas evd in |