diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9f48297613..d5c6f09760 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -847,6 +847,15 @@ let rec find_solution_type evarenv = function | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false +let find_most_recent_projection evi sols = + let sign = List.map get_id (evar_filtered_context evi) in + match sols with + | y::l -> + List.fold_right (fun (id,p as x) (id',_ as y) -> + if List.index Id.equal id sign < List.index Id.equal id' sign then x else y) + l y + | _ -> assert false + (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -1434,7 +1443,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | (id,p)::_::_ -> + | _ -> + let (id,p) = find_most_recent_projection evi sols in if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in |