Being consistent in making arbitrary choices in recursive calls to

evar_define.

Interestingly, the added choose in evarconv.ml allows solve_evar_evar
to be observationally commutative, in the sense of not either fail or
succeed in compiling the stdlib whether problems are given in the
left-to-right or right-to-left order.

2 files changed, 6 insertions, 6 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0dc796110..55fd23aa5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1060,7 +1060,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
                  (position_problem true pbty) evk1 args1 args2)
   | Evar ev1, Evar ev2 ->
       Success (solve_evar_evar ~force:true
-        (evar_define (evar_conv_x ts)) (evar_conv_x ts) env evd
+        (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
         (position_problem true pbty) ev1 ev2)
   | Evar ev1,_ when Array.length l1 <= Array.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ae2931822..b8acd6411 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1263,7 +1263,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
       let ty = lazy (Retyping.get_type_of env !evdref t) in
-      let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in
+      let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
       evdref := evd;
       c
     with
@@ -1276,7 +1276,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           let ty = find_solution_type (evar_filtered_env evi) sols in
           let ty' = instantiate_evar_array evi ty argsv in
           let (evd,evar,(evk',argsv' as ev')) =
-            materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
+            materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in
           let ts = expansions_of_var aliases t in
           let test c = isEvar c || List.mem_f Constr.equal c ts in
           let filter = restrict_upon_filter evd evk test argsv' in
@@ -1326,7 +1326,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           (* Make the virtual left evar real *)
           let ty = get_type_of env' !evdref t in
           let (evd,evar'',ev'') =
-             materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+             materialize_evar (evar_define conv_algo ~choose) env' !evdref k ev ty in
           (* materialize_evar may instantiate ev' by another evar; adjust it *)
           let (evk',args' as ev') = normalize_evar evd ev' in
           let evd =
@@ -1339,7 +1339,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
             | CannotProject filter'' ->
               (* ... or postpone the problem *)
-              postpone_evar_evar (evar_define conv_algo) env' evd None filter'' ev'' filter' ev' in
+              postpone_evar_evar (evar_define conv_algo ~choose) env' evd None filter'' ev'' filter' ev' in
           evdref := evd;
           evar'')
     | _ ->
@@ -1370,7 +1370,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             | [x] -> x
             | _ ->
               let (evd,evar'',ev'') =
-                materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+                materialize_evar (evar_define conv_algo ~choose) env' !evdref k ev ty in
               evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates);
               evar'')
         | None ->