diff options
| author | Pierre-Marie Pédrot | 2016-10-08 17:14:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-08 17:14:38 +0200 |
| commit | 82eb6cbfa3db53756ea40fb4795836d6f8c55bbe (patch) | |
| tree | 2721409ee43e729c82d5e3337d58bbbdb3f461aa /pretyping | |
| parent | 8110e9cbd6d70960a221c316774460f6ad6dc5e9 (diff) | |
| parent | 0a6f0c161756a1878dd81e438df86f08631d8399 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 7 |
3 files changed, 7 insertions, 9 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b033f5a395..b7e0535dad 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -42,12 +42,7 @@ let _ = Goptions.declare_bool_option { let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then - let c' = Some (mkProj (Projection.make cst true, c)) in - match ReductionBehaviour.get (Globnames.ConstRef cst) with - | None -> c' - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags) then None - else c' + Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 6c8677855a..a97e248aee 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1591,6 +1591,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = * ass. *) +(* This criterion relies on the fact that we postpone only problems of the form: +?x [?x1 ... ?xn] = t or the symmetric case. *) let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e6f4090f40..531b615539 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1269,8 +1269,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] @@ -1389,7 +1388,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 |