diff options
| author | Matthieu Sozeau | 2015-10-20 18:15:04 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-20 18:15:04 +0200 |
| commit | a1b828d31c73d3342345243e9fb4af69610616a0 (patch) | |
| tree | 0302cb336cc1dbecb2b5622dd2e950de40c6a44b | |
| parent | 7d6d9c5aea6232200b99e828b7e04b49808f8478 (diff) | |
Fix lemma-overloading
Update the evar_source of the solution evar in evar/evar problems to
propagate the information that it does not necessarily have to be solved
in Program mode.
| -rw-r--r-- | pretyping/evarsolve.ml | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b384bdfe16..f06207c3b9 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1149,10 +1149,19 @@ let check_evar_instance evd evk1 body conv_algo = | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) +let update_evar_source ev1 ev2 evd = + let loc, evs2 = evar_source ev2 evd in + match evs2 with + | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> + let evi = Evd.find evd ev1 in + Evd.add evd ev1 {evi with evar_source = loc, evs2} + | _ -> evd + 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_source (fst (destEvar body)) evk2 evd' in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c @@ -1164,8 +1173,8 @@ let preferred_orientation evd evk1 evk2 = let _,src2 = (Evd.find_undefined evd evk2).evar_source in (* This is a heuristic useful for program to work *) match src1,src2 with - | Evar_kinds.QuestionMark _, _ -> true - | _,Evar_kinds.QuestionMark _ -> false + | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true + | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false | _ -> true let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = |