Flags of evar_conv_x/unifiers: rationalize

6 files changed, 125 insertions, 118 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 57725dbdc1..3b904570d4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1709,8 +1709,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
         let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
         begin
           let flags = (default_flags_of TransparentState.full) in
-          let conv = conv_fun evar_conv_x flags in
-          match solve_simple_eqn conv !!env sigma (None,ev,substl inst ev') with
+          match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with
           | Success evd -> evdref := evd
           | UnifFailure _ -> assert false
         end;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8f7c88b0db..29fdd1a44c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -462,13 +462,13 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
 	in
           begin match EConstr.kind evd term1, EConstr.kind evd term2 with
           | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
-            (match solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd
+            (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
               (position_problem true pbty,ev,term2) with
 	      | UnifFailure (_,OccurCheck _) -> 
 		(* Eta-expansion might apply *) default ()
 	      | x -> x)
           | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
-            (match solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd
+            (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
               (position_problem false pbty,ev,term1) with
 	      | UnifFailure (_, OccurCheck _) ->
 		(* Eta-expansion might apply *) default () 
@@ -487,7 +487,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       | Some l1' -> (* Miller-Pfenning's patterns unification *)
 	let t2 = tM in
 	let t2 = solve_pattern_eqn env evd l1' t2 in
-          solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd
+          solve_simple_eqn (conv_fun evar_conv_x) flags env evd
 	    (position_problem on_left pbty,ev,t2) 
   in
   let consume_stack on_left (termF,skF) (termO,skO) evd =
@@ -668,7 +668,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
        (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
        let ev1' = whd_evar i' t1 in
        if isEvar i' ev1' then
-         solve_simple_eqn flags (conv_fun evar_conv_x flags) env i'
+         solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem true pbty,destEvar i' ev1',term2)
        else
          evar_eqappr_x flags env evd pbty
@@ -678,7 +678,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
        (* we now unify r[?ev1] and ?ev2 *)
        let ev2' = whd_evar i' t2 in
        if isEvar i' ev2' then
-         solve_simple_eqn flags (conv_fun evar_conv_x flags) env i'
+         solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r))
        else
          evar_eqappr_x flags env evd pbty
@@ -689,7 +689,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
        (* we now unify ?ev1 and r[?ev2] *)
        let ev1' = whd_evar i' t1 in
        if isEvar i' ev1' then
-         solve_simple_eqn flags (conv_fun evar_conv_x flags) env i'
+         solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r))
        else evar_eqappr_x flags env evd pbty
                           ((ev1', sk1), csts1) ((term2, sk2), csts2)
@@ -737,13 +737,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           if Evar.equal sp1 sp2 then
             match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
 	    |None, Success i' ->
-              Success (solve_refl flags (fun p env i pbty a1 a2 ->
+              Success (solve_refl (fun flags p env i pbty a1 a2 ->
                 let flags =
                   match p with
                   | TypeUnification -> default_flags env
                   | TermUnification -> flags
                 in
-                is_success (evar_conv_x flags env i pbty a1 a2))
+                is_success (evar_conv_x flags env i pbty a1 a2)) flags
                 env i' (position_problem true pbty) sp1 al1 al2)
 	    |_, (UnifFailure _ as x) -> x
             |Some _, _ -> UnifFailure (i,NotSameArgSize)
@@ -972,15 +972,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           if Evar.equal sp1 sp2 then
             match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with
             |None, Success i' ->
-              (** FIXME: solve_refl can restrict the evar, do we want to allow that? *)
-              Success (solve_refl flags (fun p env i pbty a1 a2 ->
-                let flags =
-                  match p with
-                  | TypeUnification -> default_flags env
-                  | TermUnification -> flags
-                in
-                is_success (evar_conv_x flags env i pbty a1 a2))
-                env i' (position_problem true pbty) sp1 al1 al2)
+              ise_array2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2
             |_, (UnifFailure _ as x) -> x
             |Some _, _ -> UnifFailure (evd,NotSameArgSize)
           else UnifFailure (evd,NotSameHead)
@@ -1106,6 +1098,8 @@ and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 =
 
 let evar_conv_x flags = evar_conv_x flags
 
+let evar_unify = conv_fun evar_conv_x
+
 (* Profiling *)
 let evar_conv_x =
   if Flags.profile then
@@ -1134,7 +1128,7 @@ let first_order_unification flags env evd (ev1,l1) (term2,l2) =
         evar_conv_x flags env i CONV t2 (mkEvar ev1)
       else
         solve_simple_eqn ~choose:true ~imitate_defs:false
-                         flags (conv_fun evar_conv_x flags) env i (None,ev1,t2))]
+          evar_unify flags env i (None,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find_undefined evd evk in
@@ -1424,11 +1418,11 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
                     if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then
                       raise (TypingFailed evd);
                     let evd = Evd.define ev (EConstr.of_constr t) evd in
-                    check_evar_instance evd ev (EConstr.of_constr t) (conv_fun evar_conv_x flags)
+                    check_evar_instance evar_unify flags evd ev (EConstr.of_constr t)
                  | Some l when abstract = Abstraction.Abstract &&
                      List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l ->
                     let evd = Evd.define ev vid evd in
-                    check_evar_instance evd ev vid (conv_fun evar_conv_x flags)
+                    check_evar_instance evar_unify flags evd ev vid
                  | _ -> evd)
               with e -> user_err (Pp.str "Cannot find an instance")
             else
@@ -1474,8 +1468,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
            evdref := evd;
            if !debug_ho_unification then
              Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv (nf_evar !evdref rhs'));
-           Evarsolve.check_evar_instance !evdref evk rhs'
-                                         (conv_fun evar_conv_x (default_flags_of TransparentState.full))
+           let flags = default_flags_of TransparentState.full in
+           Evarsolve.check_evar_instance evar_unify flags !evdref evk rhs'
          with IllTypedInstance _ -> raise (TypingFailed evd)
        in Evd.define evk rhs' evd
   in
@@ -1554,19 +1548,20 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
          let reason = ProblemBeyondCapabilities in
          UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
   | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
-     let f ontype env evd pbty x y =
+     let f flags ontype env evd pbty x y =
        let reds =
          match ontype with
          | TypeUnification -> full_transparent_state
          | TermUnification -> flags.open_ts
        in is_fconv ~reds pbty env evd x y
      in
-      Success (solve_refl ~can_drop:true flags f env evd
+      Success (solve_refl ~can_drop:true f flags env evd
                  (position_problem true pbty) evk1 args1 args2)
   | Evar ev1, Evar ev2 when app_empty ->
       Success (solve_evar_evar ~force:true
-        flags (evar_define flags (conv_fun evar_conv_x flags) ~choose:true) (conv_fun evar_conv_x flags) env evd
-        (position_problem true pbty) ev1 ev2)
+                 (evar_define evar_unify flags ~choose:true)
+                 evar_unify flags 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 *)
       (* and otherwise second-order matching *)
@@ -1629,10 +1624,9 @@ let rec solve_unconstrained_evars_with_candidates flags evd =
       | a::l ->
           (* In case of variables, most recent ones come first *)
           try
-            let conv_algo = conv_fun evar_conv_x flags in
-            let evd = check_evar_instance evd evk a conv_algo in
+            let evd = check_evar_instance evar_unify flags evd evk a in
             let evd = Evd.define evk a evd in
-            match reconsider_unif_constraints conv_algo evd with
+            match reconsider_unif_constraints evar_unify flags evd with
             | Success evd -> solve_unconstrained_evars_with_candidates flags evd
             | UnifFailure _ -> aux l
           with
@@ -1650,8 +1644,8 @@ let solve_unconstrained_impossible_cases env evd =
       let j, ctx = coq_unit_judge env in
       let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
       let ty = j_type j in
-      let conv_algo = conv_fun evar_conv_x (default_flags env) in
-      let evd' = check_evar_instance evd' evk ty conv_algo in
+      let flags = default_flags env in
+      let evd' = check_evar_instance evar_unify flags evd' evk ty in
         Evd.define evk ty evd'
     | _ -> evd') evd evd
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index bd55b952a6..430dff2091 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -24,7 +24,7 @@ val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> uni
 type unify_fun = unify_flags ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
 
-val conv_fun : unify_fun -> unify_flags -> Evarsolve.unifier
+val conv_fun : unify_fun -> Evarsolve.unifier
 
 exception UnableToUnify of evar_map * Pretype_errors.unification_error
 
@@ -112,6 +112,8 @@ val set_evar_conv : unify_fun -> unit
 (** The default unification algorithm with evars and universes. *)
 val evar_conv_x : unify_fun
 
+val evar_unify : Evarsolve.unifier
+
 (**/**)
 (* For debugging *)
 val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 2ff52d1657..2d2db6a02b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -47,18 +47,24 @@ type unification_result =
 
 let is_success = function Success _ -> true | UnifFailure _ -> false
 
-let test_success conv_algo b env evd c c' rhs =
-  is_success (conv_algo b env evd c c' rhs)
-
-(** A unification function: parameterized by the kind of unification,
-    environment, sigma, conversion problem and the two terms to unify. *)
-type unifier = unification_kind ->
+let test_success unify flags b env evd c c' rhs =
+  is_success (unify flags b env evd c c' rhs)
+
+(** A unification function parameterized by:
+    - unification flags
+    - the kind of unification
+    - environment
+    - sigma
+    - conversion problem
+    - the two terms to unify. *)
+
+type unifier = unify_flags -> unification_kind ->
   env -> evar_map -> conv_pb -> constr -> constr -> unification_result
 
 (** A conversion function: parameterized by the kind of unification,
     environment, sigma, conversion problem and the two terms to convert.
     Conversion is not allowed to instantiate evars contrary to unification. *)
-type conversion_check = unification_kind ->
+type conversion_check = unify_flags -> unification_kind ->
   env ->  evar_map -> conv_pb -> constr -> constr -> bool
 
 let normalize_evar evd ev =
@@ -177,7 +183,7 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
 
 exception IllTypedInstance of env * EConstr.types * EConstr.types
 
-let recheck_applications conv_algo env evdref t =
+let recheck_applications unify flags env evdref t =
   let rec aux env t =
     match EConstr.kind !evdref t with
     | App (f, args) ->
@@ -188,7 +194,7 @@ let recheck_applications conv_algo env evdref t =
 	 if i < Array.length argsty then
 	 match EConstr.kind !evdref (whd_all env !evdref ty) with
 	 | Prod (na, dom, codom) ->
-            (match conv_algo TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with
+            (match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
 			     aux (succ i) (subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
@@ -757,7 +763,7 @@ let restrict_upon_filter evd evk p args =
   let len = Array.length args in
   Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i))
 
-let check_evar_instance evd evk1 body conv_algo =
+let check_evar_instance unify flags evd evk1 body =
   let evi = Evd.find evd evk1 in
   let evenv = evar_env evi in
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
@@ -766,7 +772,7 @@ let check_evar_instance evd evk1 body conv_algo =
     try Retyping.get_type_of ~lax:true evenv evd body
     with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
   in
-  match conv_algo TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
+  match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
@@ -905,13 +911,13 @@ let rec find_solution_type evarenv = function
  * pass [define] to [do_projection_effects] as a parameter.
  *)
 
-let rec do_projection_effects conv_algo define_fun env ty evd = function
+let rec do_projection_effects unify flags define_fun env ty evd = function
   | ProjectVar -> evd
   | ProjectEvar ((evk,argsv),evi,id,p) ->
-      let evd = check_evar_instance evd evk (mkVar id) conv_algo in
+      let evd = check_evar_instance unify flags evd evk (mkVar id) in
       let evd = Evd.define evk (EConstr.mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
-      let evd = do_projection_effects conv_algo define_fun env ty evd p in
+      let evd = do_projection_effects unify flags define_fun env ty evd p in
       let ty = whd_all env evd (Lazy.force ty) in
       if not (isSort evd ty) then
         (* Don't try to instantiate if a sort because if evar_concl is an
@@ -1147,9 +1153,9 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
  * Note: argument f is the function used to instantiate evars.
  *)
 
-let filter_compatible_candidates conv_algo env evd evi args rhs c =
+let filter_compatible_candidates unify flags env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
-  match conv_algo TermUnification env evd Reduction.CONV rhs c' with
+  match unify flags TermUnification env evd Reduction.CONV rhs c' with
   | Success evd -> Some (c,evd)
   | UnifFailure _ -> None
 
@@ -1159,7 +1165,7 @@ let filter_compatible_candidates conv_algo env evd evi args rhs c =
 
 exception DoesNotPreserveCandidateRestriction
 
-let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
+let restrict_candidates unify flags env evd filter1 (evk1,argsv1) (evk2,argsv2) =
   let evi1 = Evd.find evd evk1 in
   let evi2 = Evd.find evd evk2 in
   match evi1.evar_candidates, evi2.evar_candidates with
@@ -1170,7 +1176,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
       let l1' = List.filter (fun c1 ->
         let c1' = instantiate_evar_array evi1 c1 argsv1 in
         let filter c2 =
-          let compatibility = filter_compatible_candidates conv_algo env evd evi2 argsv2 c1' c2 in
+          let compatibility = filter_compatible_candidates unify flags env evd evi2 argsv2 c1' c2 in
           match compatibility with
           | None -> false
           | Some _ -> true
@@ -1237,14 +1243,14 @@ exception EvarSolvedOnTheFly of evar_map * EConstr.constr
 
 (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
    the common domain of definition *)
-let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+let project_evar_on_evar force unify flags env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion env evd aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
     (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
     argsv1 in
   let candidates1 =
-    try restrict_candidates g env evd filter1 ev1 ev2
+    try restrict_candidates unify flags env evd filter1 ev1 ev2
     with DoesNotPreserveCandidateRestriction ->
       let evd,ev1' = do_restrict_hyps evd ev1 filter1 NoUpdate in
       raise (CannotProject (evd,ev1')) in
@@ -1268,16 +1274,16 @@ let update_evar_info ev1 ev2 evd =
   let evi = Evd.find evd ev2 in
   Evd.add evd ev2 {evi with evar_source = loc, evs1}
 
-let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
+let solve_evar_evar_l2r force f unify flags 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,body = project_evar_on_evar force unify flags env evd aliases 0 pbty ev1 ev2 in
     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
+    check_evar_instance unify flags evd' evk2 body
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
 
@@ -1289,26 +1295,26 @@ let preferred_orientation evd evk1 evk2 =
   else true
 
 (** Precondition evk1 is not frozen, evk2 might be. *)
-let solve_evar_evar_aux force flags f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env evd in
   let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in
   if preferred_orientation evd evk1 evk2 then
-    try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
+    try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) when not frozen_ev2 ->
-    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
+    try solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
     add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
     try if not frozen_ev2 then
-          solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
+          solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
         else raise (CannotProject (evd,ev1))
     with CannotProject (evd,ev1) ->
-    try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
+    try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
     add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 (** Precondition: evk1 is not frozen *)
-let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+let solve_evar_evar ?(force=false) f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let pbty = if force then None else pbty in
   let evi = Evd.find evd evk1 in
   let downcast evk t evd = downcast evk t evd in
@@ -1343,14 +1349,14 @@ let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (e
           downcast evk2 t2 (downcast evk1 t1 evd)
     with Reduction.NotArity -> 
       evd in
-  solve_evar_evar_aux force flags f g env evd pbty ev1 ev2
+  solve_evar_evar_aux force f unify flags env evd pbty ev1 ev2
 
 (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
  * definitions. We try to unify the ti with the ui pairwise. The pairs
  * that don't unify are discarded (i.e. ?e is redefined so that it does not
  * depend on these args). *)
 
-let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2 =
+let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 =
   let evdref = ref evd in
   let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
   | None -> false
@@ -1363,19 +1369,19 @@ let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
     restrict_upon_filter evd evk
-      (fun (a1,a2) -> conv_algo TermUnification env evd Reduction.CONV a1 a2) args in
+      (fun (a1,a2) -> unify flags TermUnification env evd Reduction.CONV a1 a2) args in
   let candidates = filter_candidates evd evk untypedfilter NoUpdate in
   let filter = closure_of_filter evd evk untypedfilter in
-  let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
-  if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
+  let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
+  if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd' else
     (* either progress, or not allowed to drop, e.g. to preserve possibly *)
     (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
     (* if e can depend on x until ?y is not resolved, or, conversely, we *)
     (* don't know if ?y has to be unified with ?y, until e is resolved *)
-  let argsv2 = restrict_instance evd evk filter argsv2 in
+  let argsv2 = restrict_instance evd' evk filter argsv2 in
   let ev2 = (fst ev1,argsv2) in
   (* Leave a unification problem *)
-  add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+  add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd'
 
 (* If the evar can be instantiated by a finite set of candidates known
    in advance, we check which of them apply *)
@@ -1383,14 +1389,14 @@ let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2
 exception NoCandidates
 exception IncompatibleCandidates
 
-let solve_candidates conv_algo env evd (evk,argsv) rhs =
+let solve_candidates unify flags env evd (evk,argsv) rhs =
   let evi = Evd.find evd evk in
   match evi.evar_candidates with
   | None -> raise NoCandidates
   | Some l ->
       let l' =
         List.map_filter
-          (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs c) l in
+          (fun c -> filter_compatible_candidates unify flags env evd evi argsv rhs c) l in
       match l' with
       | [] -> raise IncompatibleCandidates
       | [c,evd] ->
@@ -1398,7 +1404,7 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
           (* time and the evar been solved by the filtering process *)
          if Evd.is_undefined evd evk then
            let evd' = Evd.define evk c evd in
-	     check_evar_instance evd' evk c conv_algo
+             check_evar_instance unify flags evd' evk c
 	 else evd
       | l when List.length l < List.length l' ->
           let candidates = List.map fst l in
@@ -1451,7 +1457,7 @@ exception NotEnoughInformationEvarEvar of EConstr.constr
 exception OccurCheckIn of evar_map * EConstr.constr
 exception MetaOccurInBodyInternal
 
-let rec invert_definition flags conv_algo choose imitate_defs
+let rec invert_definition unify flags choose imitate_defs
                           env evd pbty (evk,argsv as ev) rhs =
   let aliases = make_alias_map env evd in
   let evdref = ref evd in
@@ -1471,7 +1477,7 @@ let rec invert_definition flags conv_algo choose imitate_defs
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
       let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
-      let evd = do_projection_effects conv_algo (evar_define flags conv_algo ~choose) env ty !evdref p in
+      let evd = do_projection_effects unify flags (evar_define unify flags ~choose) env ty !evdref p in
       evdref := evd;
       c
     with
@@ -1484,7 +1490,7 @@ let rec invert_definition flags conv_algo choose imitate_defs
           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 flags conv_algo ~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
@@ -1525,7 +1531,7 @@ let rec invert_definition flags conv_algo choose imitate_defs
         let aliases = lift_aliases k aliases in
         (try
           let ev = (evk,Array.map (lift k) argsv) in
-          let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
+          let evd,body = project_evar_on_evar false unify flags env' !evdref aliases k None ev' ev in
           evdref := evd;
           body
         with
@@ -1536,15 +1542,15 @@ let rec invert_definition flags conv_algo choose imitate_defs
           (* Make the virtual left evar real *)
           let ty = get_type_of env' evd t in
           let (evd,evar'',ev'') =
-             materialize_evar (evar_define flags conv_algo ~choose) env' evd k ev ty in
+             materialize_evar (evar_define unify flags ~choose) env' evd 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 =
              (* Try to project (a restriction of) the left evar ... *)
             try
-              let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
+              let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in
               let evd = Evd.define evk' body evd in
-		check_evar_instance evd evk' body conv_algo
+                check_evar_instance unify flags evd evk' body
             with
             | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
             | CannotProject (evd,ev'') ->
@@ -1581,7 +1587,7 @@ let rec invert_definition flags conv_algo choose imitate_defs
             | [x] -> x
             | _ ->
               let (evd,evar'',ev'') =
-                materialize_evar (evar_define flags conv_algo ~choose) env' !evdref k ev ty in
+                materialize_evar (evar_define unify flags ~choose) env' !evdref k ev ty in
               evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates);
               evar'')
         | None ->
@@ -1611,7 +1617,7 @@ let rec invert_definition flags conv_algo choose imitate_defs
     else
       let t' = imitate (env,0) rhs in
 	if !progress then
-	  (recheck_applications conv_algo (evar_env evi) evdref t'; t')
+          (recheck_applications unify flags (evar_env evi) evdref t'; t')
 	else t'
   in (!evdref,body)
 
@@ -1623,30 +1629,31 @@ let rec invert_definition flags conv_algo choose imitate_defs
  * ev is assumed not to be frozen.
  *)
 
-and evar_define flags conv_algo ?(choose=false) ?(imitate_defs=true) env evd pbty (evk,argsv as ev) rhs =
+and evar_define unify flags ?(choose=false) ?(imitate_defs=true) env evd pbty (evk,argsv as ev) rhs =
   match EConstr.kind evd rhs with
   | Evar (evk2,argsv2 as ev2) ->
       if Evar.equal evk evk2 then
-        solve_refl ~can_drop:choose flags
-          (test_success conv_algo) env evd pbty evk argsv argsv2
+        solve_refl ~can_drop:choose
+          (test_success unify) flags env evd pbty evk argsv argsv2
       else
-        solve_evar_evar ~force:choose flags
-          (evar_define flags conv_algo) conv_algo env evd pbty ev ev2
+        solve_evar_evar ~force:choose
+          (evar_define unify flags) unify flags env evd pbty ev ev2
   | _ ->
-  try solve_candidates conv_algo env evd ev rhs
+  try solve_candidates unify flags env evd ev rhs
   with NoCandidates ->
   try
-    let (evd',body) = invert_definition flags conv_algo choose imitate_defs env evd pbty ev rhs in
+    let (evd',body) = invert_definition unify flags choose imitate_defs env evd pbty ev rhs in
     if occur_meta evd' body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
     if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
-    let evd' = Evd.define evk body evd' in
-    (** Check after definition, as checking could involve the same
-        evar definition problem again otherwise *)
-    check_evar_instance evd' evk body conv_algo
+    (** Check instance freezing the evar to be defined, as
+        checking could involve the same evar definition problem again otherwise *)
+    let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in
+    let evd' = check_evar_instance unify flags evd' evk body in
+    Evd.define evk body evd'
   with
     | NotEnoughInformationToProgress sols ->
         postpone_non_unique_projection env evd pbty ev sols rhs
@@ -1661,7 +1668,7 @@ and evar_define flags conv_algo ?(choose=false) ?(imitate_defs=true) env evd pbt
         let c = whd_all env evd rhs in
         match EConstr.kind evd c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
-            solve_refl flags (fun _b env sigma pb c c' -> is_fconv pb env sigma c c')
+            solve_refl (fun flags _b env sigma pb c c' -> is_fconv pb env sigma c c') flags
                        env evd pbty evk argsv argsv2
         | _ ->
 	    raise (OccurCheckIn (evd,rhs))
@@ -1696,13 +1703,13 @@ let status_changed evd lev (pbty,_,t1,t2) =
   (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) ||
   (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false)
 
-let reconsider_unif_constraints conv_algo evd =
+let reconsider_unif_constraints unify flags evd =
   let (evd,pbs) = extract_changed_conv_pbs evd (status_changed evd) in
   List.fold_left
     (fun p (pbty,env,t1,t2 as x) ->
        match p with
        | Success evd ->
-           (match conv_algo TermUnification env evd pbty t1 t2 with
+           (match unify flags TermUnification env evd pbty t1 t2 with
            | Success _ as x -> x
            | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e)))
        | UnifFailure _ as x -> x)
@@ -1715,12 +1722,12 @@ let reconsider_unif_constraints conv_algo evd =
  * if the problem couldn't be solved. *)
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn flags conv_algo ?(choose=false) ?(imitate_defs=true)
+let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true)
                      env evd (pbty,(evk1,args1 as ev1),t2) =
   try
     let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
-    let evd = evar_define flags conv_algo ~choose ~imitate_defs env evd pbty ev1 t2 in
-      reconsider_unif_constraints conv_algo evd
+    let evd = evar_define unify flags ~choose ~imitate_defs env evd pbty ev1 t2 in
+      reconsider_unif_constraints unify flags evd
   with
     | NotInvertibleUsingOurAlgorithm t ->
         UnifFailure (evd,NotClean (ev1,env,t))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 87804f01b6..810796457f 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -35,11 +35,6 @@ val is_success : unification_result -> bool
    their representative that is most ancient in the context *)
 val expand_vars_in_term : env -> evar_map -> constr -> constr
 
-(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
-   possibly solving related unification problems, possibly leaving open
-   some problems that cannot be solved in a unique way (except if choose is
-   true); fails if the instance is not valid for the given [ev] *)
-
 (** One might want to use different conversion strategies for types and terms:
     e.g. preventing delta reductions when doing term unifications but allowing
     arbitrary delta conversion when checking the types of evar instances. *)
@@ -48,18 +43,28 @@ type unification_kind =
   | TypeUnification
   | TermUnification
 
-(** A unification function: parameterized by the kind of unification,
-    environment, sigma, conversion problem and the two terms to unify. *)
-type unifier = unification_kind ->
+(** A unification function parameterized by:
+    - unification flags
+    - the kind of unification
+    - environment
+    - sigma
+    - conversion problem
+    - the two terms to unify. *)
+type unifier = unify_flags -> unification_kind ->
   env -> evar_map -> conv_pb -> constr -> constr -> unification_result
 
 (** A conversion function: parameterized by the kind of unification,
     environment, sigma, conversion problem and the two terms to convert.
     Conversion is not allowed to instantiate evars contrary to unification. *)
-type conversion_check = unification_kind ->
-  env ->  evar_map -> conv_pb -> constr -> constr -> bool
+type conversion_check = unify_flags -> unification_kind ->
+  env -> evar_map -> conv_pb -> constr -> constr -> bool
+
+(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
+   possibly solving related unification problems, possibly leaving open
+   some problems that cannot be solved in a unique way (except if choose is
+   true); fails if the instance is not valid for the given [ev] *)
 
-val evar_define : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool ->
+val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool ->
   env -> evar_map -> bool option -> existential -> constr -> evar_map
 
 val refresh_universes :
@@ -71,18 +76,18 @@ val refresh_universes :
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
-val solve_refl : ?can_drop:bool -> unify_flags -> conversion_check -> env ->  evar_map ->
+val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env ->  evar_map ->
   bool option -> Evar.t -> constr array -> constr array -> evar_map
 
-val solve_evar_evar : ?force:bool -> unify_flags ->
+val solve_evar_evar : ?force:bool ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
-  unifier ->
+  unifier -> unify_flags ->
   env ->  evar_map -> bool option -> existential -> existential -> evar_map
 
-val solve_simple_eqn : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
+val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env ->  evar_map ->
   bool option * existential * constr -> unification_result
 
-val reconsider_unif_constraints : unifier -> evar_map -> unification_result
+val reconsider_unif_constraints : unifier -> unify_flags -> evar_map -> unification_result
 
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> alias list option
@@ -97,8 +102,8 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
 exception IllTypedInstance of env * types * types
 
 (* May raise IllTypedInstance if types are not convertible *)
-val check_evar_instance :
-  evar_map -> Evar.t -> constr -> unifier -> evar_map
+val check_evar_instance : unifier -> unify_flags ->
+  evar_map -> Evar.t -> constr -> evar_map
 
 val remove_instance_local_defs :
   evar_map -> Evar.t -> 'a array -> 'a list
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 486aa38558..3de8c381d0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1325,7 +1325,7 @@ let order_metas metas =
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
 let solve_simple_evar_eqn flags env evd ev rhs =
-  match solve_simple_eqn flags (Evarconv.conv_fun Evarconv.evar_conv_x flags) env evd (None,ev,rhs) with
+  match solve_simple_eqn Evarconv.evar_unify flags env evd (None,ev,rhs) with
   | UnifFailure (evd,reason) ->
       error_cannot_unify env evd ~reason (mkEvar ev,rhs);
   | Success evd -> evd