diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9422a96f21..674f6846ae 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1239,26 +1239,21 @@ let check_evar_instance evd evk1 body conv_algo = | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) let update_evar_info ev1 ev2 evd = + (* We update the source of obligation evars during evar-evar unifications. *) let loc, evs2 = evar_source ev2 evd in - let evd = - (* We keep the obligation evar flag during evar-evar unifications *) - if is_obligation_evar evd ev2 then - let evi = Evd.find evd ev1 in - let evd = Evd.add evd ev1 {evi with evar_source = loc, evs2} in - Evd.set_obligation_evar evd ev1 - else evd - in - (** [ev1] inherits the unresolvability status from [ev2] *) - if not (Evd.is_resolvable_evar evd ev2) then - Evd.set_resolvable_evar evd ev1 false - else evd + let evi = Evd.find evd ev1 in + Evd.add evd ev1 {evi with evar_source = loc, evs2} let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in - let evd' = Evd.define evk2 body evd in - let evd' = update_evar_info (fst (destEvar evd body)) evk2 evd' in - check_evar_instance evd' evk2 body g + let evd' = Evd.define_with_evar evk2 body evd in + let evd' = + if is_obligation_evar evd evk2 then + update_evar_info evk2 (fst (destEvar evd' body)) evd' + else evd' + in + check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c |