diff options
| author | msozeau | 2013-07-19 14:50:48 +0000 |
|---|---|---|
| committer | msozeau | 2013-07-19 14:50:48 +0000 |
| commit | f5bbb5ce34bb1ee2165086b0fdb3ee5f3d96a44e (patch) | |
| tree | 6471c4c429f32757813bcfe0685f9b0b1957ed57 /pretyping/unification.ml | |
| parent | 1b701c4f6f6ebf9fc39720fdb3c2990cfc884766 (diff) | |
- Fix uncaught exception NotASort from reductionops, moving decomp_sort to retyping.ml
- In unification's w_merge, assign the evars in the same order they were found. Might
create rare incompatibilities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16632 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -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 5dd7942437..14d6ad333f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -950,7 +950,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) (List.rev evars) [] let w_unify_meta_types env ?(flags=default_unify_flags) evd = let metas,evd = retract_coercible_metas evd in |