diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-08 17:41:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-08 17:41:15 +0200 |
| commit | 1a9fe0dfe837ccbee25e9ecf19a7b2e7768a7958 (patch) | |
| tree | d0539f4fe40c2a3077858c6c69440d98de053964 /pretyping/unification.ml | |
| parent | 2dcd8f2e82366bb3b0f51a42426ccdfbb00281dc (diff) | |
| parent | 82eb6cbfa3db53756ea40fb4795836d6f8c55bbe (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5d6c41103..a96a496b8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1270,8 +1270,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - Evarconv.consider_remaining_unif_problems env evd + | Success evd -> evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] @@ -1390,7 +1389,9 @@ let w_merge env with_types flags (evd,metas,evars) = in w_merge_rec evd [] [] eqns in let res = (* merge constraints *) - w_merge_rec evd (order_metas metas) (List.rev evars) [] + w_merge_rec evd (order_metas metas) + (* Assign evars in the order of assignments during unification *) + (List.rev evars) [] in if with_types then check_types res else res |