Fixing a (known) "bugged" part of imitation in unification.

We ensure that when imitation stops to be possible, we postpone an
equation of the type of the subterm (and not of the arbitrary type of
an evar possibly depending on this subterm).

1 files changed, 4 insertions, 11 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 715b80f428..994ba9e0e7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -935,13 +935,6 @@ let project_with_effects aliases sigma t subst =
   in
   filter_solution (Int.Map.fold is_projectable subst [])
 
-open Context.Named.Declaration
-let rec find_solution_type evarenv = function
-  | (id,ProjectVar)::l -> get_type (lookup_named id evarenv)
-  | [id,ProjectEvar _] -> (* bugged *) get_type (lookup_named id evarenv)
-  | (id,ProjectEvar _)::l -> find_solution_type evarenv l
-  | [] -> 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
@@ -1552,10 +1545,10 @@ let rec invert_definition unify flags choose imitate_defs
             raise (NotEnoughInformationToProgress sols);
           (* No unique projection but still restrict to where it is possible *)
           (* materializing is necessary, but is restricting useful? *)
-          let ty = find_solution_type (evar_filtered_env env evi) sols in
-          let ty' = instantiate_evar_array evi ty argsv in
+          let t' = of_alias t in
+          let ty = Retyping.get_type_of env !evdref t' in
           let (evd,evar,(evk',argsv' as ev')) =
-            materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in
+            materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty in
           let ts = expansions_of_var evd aliases t in
           let test c = isEvar evd c || List.exists (is_alias evd c) ts in
           let filter = restrict_upon_filter evd evk test argsv' in
@@ -1564,7 +1557,7 @@ let rec invert_definition unify flags choose imitate_defs
           let evd = match candidates with
           | NoUpdate ->
             let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in
-            add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',of_alias t) evd
+            add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t') evd
           | UpdateWith _ ->
             restrict_evar evd evk' filter candidates
           in