diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-11 14:34:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-11 17:42:09 +0100 |
| commit | d083200ae5b391ceffaa0329a8e3a334036c7968 (patch) | |
| tree | 07fedfe7b3a8da2cf46baff314b8e3c93e7dfa8d | |
| parent | 6c3f6abd15ebf095112a2abd0136536ea8922b6c (diff) | |
Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.
This fixes current failure of RelationAlgebra.
| -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 a53240a1c..40b81dd4c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1368,7 +1368,7 @@ let w_unify_core_0 env evd with_types cv_pb flags m n = let (mc1,evd') = retract_coercible_metas evd in let (sigma,ms,es) = check_types env (set_flags_for_type flags.core_unify_flags) (evd,mc1,[]) m n in let subst2 = - unify_0_with_initial_metas (evd',ms,es) false env cv_pb + unify_0_with_initial_metas (sigma,ms,es) false env cv_pb flags.core_unify_flags m n in let evd = w_merge env with_types flags.merge_unify_flags subst2 in |