Merge PR #7819: Ho matching occ sel

Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot

33 files changed, 1249 insertions, 626 deletions

diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh
new file mode 100644
index 0000000000..2b4c1489ad
--- /dev/null
+++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh
@@ -0,0 +1,13 @@
+_OVERLAY_BRANCH=ho-matching-occ-sel
+
+if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    unicoq_CI_REF="PR7819-overlay"
+
+    mtac2_CI_REF="PR7819-overlay"
+    mtac2_CI_GITURL=https://github.com/mattam82/Mtac2
+
+    equations_CI_GITURL=https://github.com/mattam82/Coq-Equations
+    equations_CI_REF="PR7819-overlay"
+
+fi
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index d70c009c6d..840c14b241 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -424,8 +424,8 @@ let new_pure_evar_full evd ?typeclass_candidate evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate
-    ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
+    ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ =
   let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -441,6 +441,7 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
     evar_concl = typ;
     evar_body = Evar_empty;
     evar_filter = filter;
+    evar_abstract_arguments = abstract_arguments;
     evar_source = src;
     evar_candidates = candidates }
   in
@@ -452,11 +453,12 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
   in
   (evd, newevk)
 
-let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
+    ?principal sign evd typ instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in
+  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
 let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
@@ -469,7 +471,8 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
+    ?principal ?hypnaming env evd typ =
   let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
   let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -477,7 +480,8 @@ let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?h
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance
+  new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+    ?typeclass_candidate ?principal instance
 
 let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 23b240f1a0..bb0da44103 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -42,7 +42,7 @@ type naming_mode =
 
 val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list ->
+  ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?typeclass_candidate:bool ->
   ?principal:bool -> ?hypnaming:naming_mode ->
@@ -50,7 +50,7 @@ val new_evar :
 
 val new_pure_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list ->
+  ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?typeclass_candidate:bool ->
   ?principal:bool ->
@@ -80,7 +80,8 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
-  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?typeclass_candidate:bool ->
   ?principal:bool ->
diff --git a/engine/evd.ml b/engine/evd.ml
index f0433d3387..dd2be29bd9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -126,6 +126,19 @@ struct
 
 end
 
+module Abstraction = struct
+
+  type abstraction =
+    | Abstract
+    | Imitate
+
+  type t = abstraction list
+
+  let identity = []
+
+  let abstract_last l = Abstract :: l
+end
+
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
@@ -143,6 +156,7 @@ type evar_info = {
   evar_hyps : named_context_val;
   evar_body : evar_body;
   evar_filter : Filter.t;
+  evar_abstract_arguments : Abstraction.t;
   evar_source : Evar_kinds.t Loc.located;
   evar_candidates : constr list option; (* if not None, list of allowed instances *)}
 
@@ -151,6 +165,7 @@ let make_evar hyps ccl = {
   evar_hyps = hyps;
   evar_body = Evar_empty;
   evar_filter = Filter.identity;
+  evar_abstract_arguments = Abstraction.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
   evar_candidates = None; }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index d2d18ca486..b0fcddb068 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -77,6 +77,18 @@ sig
 
 end
 
+module Abstraction : sig
+  type abstraction =
+    | Abstract
+    | Imitate
+
+  type t = abstraction list
+
+  val identity : t
+
+  val abstract_last : t -> t
+end
+
 (** {6 Evar infos} *)
 
 type evar_body =
@@ -94,6 +106,10 @@ type evar_info = {
   (** Boolean mask over {!evar_hyps}. Should have the same length.
       When filtered out, the corresponding variable is not allowed to occur
       in the solution *)
+  evar_abstract_arguments : Abstraction.t;
+  (** Boolean information over {!evar_hyps}, telling if an hypothesis instance
+      can be imitated or should stay abstract in HO unification problems
+      and inversion (see [second_order_matching_with_args] for its use). *)
   evar_source : Evar_kinds.t located;
   (** Information about the evar. *)
   evar_candidates : econstr list option;
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8da30bd9c9..6fd2f7c2bc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       raise NoChange;
     end
   in
-  let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
+  let eq_constr c1 c2 =
+    try ignore(Evarconv.unify_delay env sigma c1 c2); true
+    with Evarconv.UnableToUnify _ -> false in
   if not (noccurn sigma 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp sigma t) then nochange "not an equality";
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d833a2cde..e78d0f93a4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -449,7 +449,7 @@ let evd_convertible env evd x y =
        unsolvable constraints remain, so we check that this unification
        does not introduce any new problem. *)
     let _, pbs = Evd.extract_all_conv_pbs evd in
-    let evd' = Evarconv.the_conv_x env x y evd in
+    let evd' = Evarconv.unify_delay env evd x y in
     let _, pbs' = Evd.extract_all_conv_pbs evd' in
     if evd' == evd || problem_inclusion pbs' pbs then Some evd'
     else None
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index a1e21aab04..543d4de0fe 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -557,7 +557,7 @@ let rec intern_atomic lf ist x =
       | _ -> false
       in
       let is_onconcl = match cl.concl_occs with
-      | AllOccurrences | NoOccurrences -> true
+      | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
       | _ -> false
       in
       TacChange (None,
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 30f716d764..eac84f0543 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | _ -> false
         in
         let is_onconcl = match cl.concl_occs with
-          | AllOccurrences | NoOccurrences -> true
+          | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
         let c_interp patvars env sigma =
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 552a4048b1..fb99b87108 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a =
   loop 0
 
 let unif_HO env ise p c =
-  try Evarconv.the_conv_x env p c ise
+  try Evarconv.unify_delay env ise p c
   with Evarconv.UnableToUnify(ise, err) ->
     raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err)))
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1ad90b2953..069ba9572a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -321,9 +321,9 @@ let inh_coerce_to_ind env sigma0 loc ty tyi =
      constructor and renounce if not able to give more information *)
   (* devrait être indifférent d'exiger leq ou pas puisque pour
      un inductif cela doit être égal *)
-  match cumul env sigma expected_typ ty with
-  | Some sigma -> sigma
-  | None -> sigma0
+  match Evarconv.unify_leq_delay env sigma expected_typ ty with
+  | sigma -> sigma
+  | exception Evarconv.UnableToUnify _ -> sigma0
 
 let binding_vars_of_inductive sigma = function
   | NotInd _ -> []
@@ -431,9 +431,9 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
             let sigma, current =
               if List.is_empty deps && isEvar sigma typ then
 	      (* Don't insert coercions if dependent; only solve evars *)
-                match cumul !!(pb.env) sigma indt typ with
-                | None -> sigma, current
-                | Some sigma -> sigma, current
+                match Evarconv.unify_leq_delay !!(pb.env) sigma indt typ with
+                | exception Evarconv.UnableToUnify _ -> sigma, current
+                | sigma -> sigma, current
 	      else
                 let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
                 sigma, j.uj_val
@@ -1707,9 +1707,11 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context !!env) in
         let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
-        begin match solve_simple_eqn (evar_conv_x TransparentState.full) !!env sigma (None,ev,substl inst ev') with
-        | Success evd -> evdref := evd
-        | UnifFailure _ -> assert false
+        begin
+          let flags = (default_flags_of TransparentState.full) in
+          match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with
+          | Success evd -> evdref := evd
+          | UnifFailure _ -> assert false
         end;
         ev'
     | _ ->
@@ -1765,9 +1767,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
         let sigma, t = abstract_tycon ?loc tycon_env sigma subst tycon extenv t in
         let sigma, tt = Typing.type_of !!extenv sigma t in
         (sigma, t, tt) in
-  match cumul !!env sigma tt (mkSort s) with
-  | None -> anomaly (Pp.str "Build_tycon: should be a type.");
-  | Some sigma ->
+  match unify_leq_delay !!env sigma tt (mkSort s) with
+  | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type.");
+  | sigma ->
     sigma, { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1945,7 +1947,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 
 let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon =
   match tycon with
-    | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma j p
+    | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma
+                ~flags:(default_flags_of TransparentState.full) j p
     | None -> sigma, j
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
@@ -2187,15 +2190,15 @@ let constr_of_pat env sigma arsign pat avoid =
                 let sigma, sign, i, avoid =
 		  try
                     let env = EConstr.push_rel_context sign env in
-                    let sigma = the_conv_x_leq (EConstr.push_rel_context sign env)
-                      (lift (succ m) ty) (lift 1 apptype) sigma in
+                    let sigma = unify_leq_delay (EConstr.push_rel_context sign env) sigma
+                      (lift (succ m) ty) (lift 1 apptype) in
                     let sigma, eq_t = mk_eq sigma (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
 		      (lift 1 app) (* aliased term *)
 		    in
 		    let neq = eq_id avoid id in
                       sigma, LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid
-                  with Reduction.NotConvertible -> sigma, sign, 1, avoid
+                  with Evarconv.UnableToUnify _ -> sigma, sign, 1, avoid
 		in
 		  (* Mark the equality as a hole *)
                   sigma, pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2329b87acc..0e6aaaa408 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -64,9 +64,9 @@ let apply_coercion_args env sigma check isproj argl funj =
       | Prod (_,c1,c2) ->
         let sigma =
           if check then
-            begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with
-              | None -> raise NoCoercion
-              | Some sigma -> sigma
+            begin match Evarconv.unify_leq_delay env sigma (Retyping.get_type_of env sigma h) c1 with
+              | exception Evarconv.UnableToUnify _ -> raise NoCoercion
+              | sigma -> sigma
             end
           else sigma
         in
@@ -157,7 +157,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
   let rec coerce_unify env x y =
     let x = hnf env !evdref x and y = hnf env !evdref y in
       try
-	evdref := the_conv_x_leq env x y !evdref;
+        evdref := Evarconv.unify_leq_delay env !evdref x y;
 	None
       with UnableToUnify _ -> coerce' env x y
   and coerce' env x y : (EConstr.constr -> EConstr.constr) option =
@@ -172,7 +172,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
       let rec aux tele typ typ' i co =
 	if i < len then
 	  let hdx = l.(i) and hdy = l'.(i) in
-	    try evdref := the_conv_x_leq env hdx hdy !evdref;
+            try evdref := unify_leq_delay env !evdref hdx hdy;
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
 		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
@@ -180,8 +180,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
               let () =
-		try evdref := the_conv_x_leq env eqT eqT' !evdref
-		with UnableToUnify _ -> raise NoSubtacCoercion
+                try evdref := unify_leq_delay env !evdref eqT eqT'
+                with UnableToUnify _ -> raise NoSubtacCoercion
 	      in
 		(* Disallow equalities on arities *)
 		if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion;
@@ -466,7 +466,7 @@ let inh_coerce_to_prod ?loc ~program_mode env evd t =
       !evdref, typ'
   else (evd, t)
 
-let inh_coerce_to_fail env evd rigidonly v t c1 =
+let inh_coerce_to_fail flags env evd rigidonly v t c1 =
   if rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr c1) && Heads.is_rigid env (EConstr.Unsafe.to_constr t))
   then
     raise NoCoercion
@@ -483,13 +483,16 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
 	  | None -> evd, None, t
       with Not_found -> raise NoCoercion
     in
-      try (the_conv_x_leq env t' c1 evd, v')
+      try (unify_leq_delay ~flags env evd t' c1, v')
       with UnableToUnify _ -> raise NoCoercion
 
-let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 =
-  try (the_conv_x_leq env t c1 evd, v)
+let default_flags_of env =
+  default_flags_of TransparentState.full
+
+let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 =
+  try (unify_leq_delay ~flags env evd t c1, v)
   with UnableToUnify (best_failed_evd,e) ->
-    try inh_coerce_to_fail env evd rigidonly v t c1
+    try inh_coerce_to_fail flags env evd rigidonly v t c1
     with NoCoercion ->
       match
       EConstr.kind evd (whd_all env evd t),
@@ -520,10 +523,10 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 =
       | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t =
+let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t =
   let (evd', val') =
     try
-      inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+      inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly (Some cj.uj_val) cj.uj_type t
     with NoCoercionNoUnifier (best_failed_evd,e) ->
       try
         if program_mode then
@@ -545,15 +548,14 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t
   let val' = match val' with Some v -> v | None -> assert(false) in
     (evd',{ uj_val = val'; uj_type = t })
 
-let inh_conv_coerce_to ?loc ~program_mode resolve_tc =
-  inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false
-
-let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc =
-  inh_conv_coerce_to_gen ~program_mode resolve_tc ?loc true
+let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) =
+  inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd
+let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) =
+  inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env evd
 
-let inh_conv_coerces_to ?loc env evd t t' =
+let inh_conv_coerces_to ?loc env evd ?(flags=default_flags_of env) t t' =
   try
-    fst (inh_conv_coerce_to_fail ?loc env evd true None t t')
+    fst (inh_conv_coerce_to_fail ?loc env evd ~flags true None t t')
   with NoCoercion ->
     evd (* Maybe not enough information to unify *)
       
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index a941391125..43d4059785 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -45,17 +45,21 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool ->
     a way [t] and [j.uj_type] are convertible; it fails if no coercion is
     applicable. resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
+
 val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool ->
-  env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
+  env -> evar_map -> ?flags:Evarconv.unify_flags ->
+  unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool ->
-  env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
+  env -> evar_map -> ?flags:Evarconv.unify_flags ->
+  unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
     is coercible to an object of type [t'] adding evar constraints if needed;
     it fails if no coercion exists *)
 val inh_conv_coerces_to : ?loc:Loc.t ->
-  env -> evar_map -> types -> types -> evar_map
+  env -> evar_map -> ?flags:Evarconv.unify_flags ->
+  types -> types -> evar_map
 
 (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
     pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index bb163ddaee..8e273fb4a8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,14 +24,28 @@ open Evardefine
 open Evarsolve
 open Evd
 open Pretype_errors
-open Context.Named.Declaration
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type unify_fun = TransparentState.t ->
+type unify_flags = Evarsolve.unify_flags
+
+type unify_fun = unify_flags ->
   env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
 
+let default_transparent_state env = TransparentState.full
+(* Conv_oracle.get_transp_state (Environ.oracle env) *)
+
+let default_flags_of ?(subterm_ts=TransparentState.empty) ts =
+  { modulo_betaiota = true;
+    open_ts = ts; closed_ts = ts; subterm_ts;
+    frozen_evars = Evar.Set.empty; with_cs = true;
+    allow_K_at_toplevel = true }
+
+let default_flags env =
+  let ts = default_transparent_state env in
+  default_flags_of ts
+
 let debug_unification = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
@@ -42,6 +56,16 @@ let () = Goptions.(declare_bool_option {
   optwrite = (fun a -> debug_unification:=a);
 })
 
+let debug_ho_unification = ref (false)
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname =
+    "Print higher-order unification debug information";
+  optkey = ["Debug";"HO";"Unification"];
+  optread = (fun () -> !debug_ho_unification);
+  optwrite = (fun a -> debug_ho_unification:=a);
+})
+
 (*******************************************)
 (* Functions to deal with impossible cases *)
 (*******************************************)
@@ -101,42 +125,106 @@ type flex_kind_of_term =
   | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *)
   | Flexible of EConstr.existential
 
-let flex_kind_of_term ts env evd c sk =
+let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars
+
+let flex_kind_of_term flags env evd c sk =
   match EConstr.kind evd c with
     | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
-      Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c)
-    | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c
-    | Evar ev -> Flexible ev
+      Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term flags.open_ts env evd c)
+    | Lambda _ when not (Option.is_empty (Stack.decomp sk)) ->
+       if flags.modulo_betaiota then MaybeFlexible c
+       else Rigid
+    | Evar ev ->
+       if is_frozen flags ev then Rigid
+       else Flexible ev
     | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ -> Rigid
     | Meta _ -> Rigid
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
     | Cast _ | App _ | Case _ -> assert false
 
-let apprec_nohdbeta ts env evd c =
+let apprec_nohdbeta flags env evd c =
   let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
-  if Stack.not_purely_applicative sk
+  if flags.modulo_betaiota && Stack.not_purely_applicative sk
   then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state
-		   ts env evd Cst_stack.empty appr))
+                   flags.open_ts env evd Cst_stack.empty appr))
   else c
 
 let position_problem l2r = function
   | CONV -> None
   | CUMUL -> Some l2r
 
-let occur_rigidly (evk,_ as ev) evd t =
+(* [occur_rigidly ev evd t] tests if the evar ev occurs in a rigid
+   context in t. Precondition: t has a rigid head and is not reducible.
+
+   That function is an under approximation of occur-check, it can return
+   false even if the occur-check would succeed on the normal form.  This
+   means we might postpone unsolvable constraints which will ultimately
+   result in an occur-check after reductions. If it returns true, we
+   know that the occur-check would also return true on the normal form.
+
+   [t] is assumed to have a rigid head, which can
+   appear under a elimination context (e.g. application, match or projection).
+
+   In the inner recursive function, the result indicates if the term is
+   rigid (irreducible), normal (succession of constructors) or
+   potentially reducible. For applications, this means than an
+   occurrence of the evar in arguments should be looked at to find an
+   occur-check if the head is rigid or normal. For inductive
+   eliminations, only an occurrence in a rigid context of the
+   discriminee counts as a rigid occurrence overall, not a normal
+   occurrence which might disappear after reduction. *)
+
+type result = Rigid of bool | Normal of bool | Reducible
+
+let rigid_normal_occ = function Rigid b -> b | Normal b -> b | _ -> false
+
+let occur_rigidly flags env evd (evk,_) t =
   let rec aux t =
     match EConstr.kind evd t with
-    | App (f, c) -> if aux f then Array.exists aux c else false
-    | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ | Int _ -> true
-    | Proj (p, c) -> not (aux c)
-    | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false
+    | App (f, c) ->
+      (match aux f with
+      | Rigid b -> Rigid (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c)
+      | Normal b -> Normal (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c)
+      | Reducible -> Reducible)
+    | Construct _ -> Normal false
+    | Ind _ | Sort _ -> Rigid false
+    | Proj (p, c) ->
+      let cst = Projection.constant p in
+      let rigid = not (TransparentState.is_transparent_constant flags.open_ts cst) in
+        if rigid then aux c
+        else (* if the evar appears rigidly in c then this elimination
+                cannot reduce and we have a rigid occurrence, otherwise
+                we don't know. *)
+          (match aux c with
+          | Rigid _ as res -> res
+          | Normal b -> Reducible
+          | Reducible -> Reducible)
+    | Evar (evk',l as ev) ->
+      if Evar.equal evk evk' then Rigid true
+      else if is_frozen flags ev then
+        Rigid (Array.exists (fun x -> rigid_normal_occ (aux x)) l)
+      else Reducible
     | Cast (p, _, _) -> aux p
-    | Lambda _ | LetIn _ -> false
-    | Const _ -> false
-    | Prod (_, b, t) -> ignore(aux b || aux t); true
-    | Rel _ | Var _ -> false
-    | Case (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false
-  in try ignore(aux t); false with Occur -> true
+    | Lambda (na, t, b) -> aux b
+    | LetIn (na, _, _, b) -> aux b
+    | Const (c,_) ->
+      if TransparentState.is_transparent_constant flags.open_ts c then Reducible
+      else Rigid false
+    | Prod (_, b, t) ->
+      let b' = aux b and t' = aux t in
+      if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true
+      else Reducible
+    | Rel _ | Var _ -> Reducible
+    | Case (_,_,c,_) ->
+      (match aux c with
+      | Rigid b -> Rigid b
+      | _ -> Reducible)
+    | Meta _ | Fix _ | CoFix _ | Int _ -> Reducible
+  in
+    match aux t with
+    | Rigid b -> b
+    | Normal b -> b
+    | Reducible -> false
 
 (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
    the problem (t1 stack1) = (t2 stack2) into a problem
@@ -365,7 +453,21 @@ let compare_cumulative_instances evd variances u u' =
     Success evd
   | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
 
-let rec evar_conv_x ts env evd pbty term1 term2 =
+let conv_fun f flags on_types =
+  let typefn env evd pbty term1 term2 =
+    let flags = { (default_flags env) with
+      with_cs = flags.with_cs;
+      frozen_evars = flags.frozen_evars }
+    in f flags env evd pbty term1 term2
+  in
+  let termfn env evd pbty term1 term2 =
+    f flags env evd pbty term1 term2
+  in
+    match on_types with
+    | TypeUnification -> typefn
+    | TermUnification -> termfn
+
+let rec evar_conv_x flags env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
   let term2 = whd_head_evar evd term2 in
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
@@ -374,7 +476,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
       let e =
-          match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with
+          match infer_conv ~catch_incon:false ~pb:pbty ~ts:flags.closed_ts env evd term1 term2 with
           | Some evd -> Success evd
           | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))
           | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
@@ -389,30 +491,30 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
     | None ->
       (* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
-        let term1 = apprec_nohdbeta (fst ts) env evd term1 in
-        let term2 = apprec_nohdbeta (fst ts) env evd term2 in
+        let term1 = apprec_nohdbeta flags env evd term1 in
+        let term2 = apprec_nohdbeta flags env evd term2 in
 	let default () = 
-          evar_eqappr_x ts env evd pbty
+          evar_eqappr_x flags env evd pbty
             (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
             (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
 	in
           begin match EConstr.kind evd term1, EConstr.kind evd term2 with
-          | Evar ev, _ when Evd.is_undefined evd (fst ev) ->
-            (match solve_simple_eqn (evar_conv_x ts) env evd
-              (position_problem true pbty,ev, term2) with
+          | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+            (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) ->
-            (match solve_simple_eqn (evar_conv_x ts) env evd
-              (position_problem false pbty,ev, term1) with
+          | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+            (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 () 
 	      | x -> x)
           | _ -> default ()
         end
 
-and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
+and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
@@ -423,18 +525,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts 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 (evar_conv_x ts) 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 =
     let switch f a b = if on_left then f a b else f b a in
     let not_only_app = Stack.not_purely_applicative skO in
-    match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
+    match switch (ise_stack2 not_only_app env evd (evar_conv_x flags)) skF skO with
       |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
+        switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
       |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
-      |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
+        switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
+      |None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO
       |_, (UnifFailure _ as x) -> x
       |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
   let eta env evd onleft sk term sk' term' =
@@ -443,12 +545,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let c = nf_evar evd c1 in
     let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
-      (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
+      flags.open_ts env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
       (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
       Cst_stack.empty in
-    if onleft then evar_eqappr_x ts env' evd CONV out1 out2
-    else evar_eqappr_x ts env' evd CONV out2 out1
+    if onleft then evar_eqappr_x flags env' evd CONV out1 out2
+    else evar_eqappr_x flags env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
     let check_strict evd u u' =
@@ -504,12 +606,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     ise_and evd [(fun i ->
                 try compare_heads i
                 with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-                 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
+                 (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')]
   in
-  let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
+  let consume on_left (_, skF as apprF) (_,skM as apprM) i =
+    if not (Stack.is_empty skF && Stack.is_empty skM) then
+      consume_stack on_left apprF apprM i
+    else quick_fail i
+  in
+  let miller on_left ev (termF,skF as apprF) (termM, skM as apprM) i =
     let switch f a b = if on_left then f a b else f b a in
     let not_only_app = Stack.not_purely_applicative skM in
-    let f1 i =
       match Stack.list_of_app_stack skF with
       | None -> quick_fail evd
       | Some lF -> 
@@ -518,17 +624,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
               switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
 	    else quick_fail i)
-	  ev lF tM i
-    and consume (termF,skF as apprF) (termM,skM as apprM) i = 
-      if not (Stack.is_empty skF && Stack.is_empty skM) then
-        consume_stack on_left apprF apprM i
-      else quick_fail i
-    and delta i =
-      switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
-	     (whd_betaiota_deltazeta_for_iota_state
-  	        (fst ts) env i cstsM (vM,skM))
+            ev lF tM i
+  in
+  let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
+    let switch f a b = if on_left then f a b else f b a in
+    let delta i =
+      switch (evar_eqappr_x flags env i pbty) (apprF,cstsF)
+        (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i cstsM (vM,skM))
     in    
-    let default i = ise_try i [f1; consume apprF apprM; delta]
+    let default i = ise_try i [miller on_left ev apprF apprM;
+                               consume on_left apprF apprM;
+                               delta]
     in
       match EConstr.kind evd termM with
       | Proj (p, c) when not (Stack.is_empty skF) ->
@@ -543,13 +649,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		try 
 		  let termM' = Retyping.expand_projection env evd p c [] in
 		  let apprM', cstsM' = 
-		    whd_betaiota_deltazeta_for_iota_state
-		      (fst ts) env evd cstsM (termM',skM)
+                    whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd cstsM (termM',skM)
 		  in
 		  let delta' i = 
-		    switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') 
+                    switch (evar_eqappr_x flags env i pbty) (apprF,cstsF) (apprM',cstsM')
 		  in
-		    fun i -> ise_try i [f1; consume apprF apprM'; delta']
+                  fun i -> ise_try i [miller on_left ev apprF apprM';
+                                   consume on_left apprF apprM'; delta']
 		with Retyping.RetypeError _ ->
 		(* Happens thanks to w_unify building ill-typed terms *) 
 		  default
@@ -563,7 +669,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       match EConstr.kind evd termR with
       | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
          eta env evd false skR termR skF termF
-      | Construct u -> eta_constructor ts env evd skR u skF termF
+      | Construct u -> eta_constructor flags env evd skR u skF termF
       | _ -> UnifFailure (evd,NotSameHead)
     in
     match Stack.list_of_app_stack skF with
@@ -571,12 +677,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         ise_try evd [consume_stack on_left apprF apprR; eta]
     | Some lF ->
         let tR = Stack.zip evd apprR in
-	  miller_pfenning on_left
-	    (fun () ->
-	      ise_try evd 
-	        [eta;(* Postpone the use of an heuristic *)
-		 (fun i -> 
-		   if not (occur_rigidly ev i tR) then
+          miller_pfenning on_left
+            (fun () ->
+              ise_try evd
+                [eta;(* Postpone the use of an heuristic *)
+                 (fun i ->
+                   if not (occur_rigidly flags env i ev tR) then
                      let i,tF =
                        if isRel i tR || isVar i tR then
                          (* Optimization so as to generate candidates *)
@@ -585,95 +691,111 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                        else
                          i,Stack.zip evd apprF in
                      switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i))
-	               tF tR
-		   else
+                       tF tR
+                   else
                      UnifFailure (evd,OccurCheck (fst ev,tR)))])
-	    ev lF tR evd
+            ev lF tR evd
+  in
+  let first_order env i t1 t2 sk1 sk2 =
+    (* Try first-order unification *)
+    match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
+    | None, Success i' ->
+       (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
+       (* 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 (conv_fun evar_conv_x) flags env i'
+                          (position_problem true pbty,destEvar i' ev1',term2)
+       else
+         evar_eqappr_x flags env evd pbty
+                       ((ev1', sk1), csts1) ((term2, sk2), csts2)
+    | Some (r,[]), Success i' ->
+       (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
+       (* we now unify r[?ev1] and ?ev2 *)
+       let ev2' = whd_evar i' t2 in
+       if isEvar i' ev2' then
+         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
+                       ((ev2', sk1), csts1) ((term2, sk2), csts2)
+    | Some ([],r), Success i' ->
+       (* Symmetrically *)
+       (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
+       (* we now unify ?ev1 and r[?ev2] *)
+       let ev1' = whd_evar i' t1 in
+       if isEvar i' ev1' then
+         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)
+    | None, (UnifFailure _ as x) ->
+       (* sk1 and sk2 have no common outer part *)
+       if Stack.not_purely_applicative sk2 then
+         (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+         flex_rigid true (destEvar evd t1) appr1 appr2
+       else
+         if Stack.not_purely_applicative sk1 then
+           (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+           flex_rigid false (destEvar evd t2) appr2 appr1
+         else
+           (* We could instead try Miller unification, then
+              postpone to see if other equations help, as in:
+              [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *)
+           x
+    | Some _, Success _ ->
+       (* sk1 and sk2 have a common outer part *)
+       if Stack.not_purely_applicative sk2 then
+         (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+         flex_rigid true (destEvar evd t1) appr1 appr2
+       else
+         if Stack.not_purely_applicative sk1 then
+           (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+           flex_rigid false (destEvar evd t2) appr2 appr1
+         else
+           (* We could instead try Miller unification, then
+              postpone to see if other equations help, as in:
+              [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *)
+           UnifFailure (i,NotSameArgSize)
+    | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")
   in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
 	     let open Pp in
              Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
-  match (flex_kind_of_term (fst ts) env evd term1 sk1, 
-	 flex_kind_of_term (fst ts) env evd term2 sk2) with
-    | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
+  match (flex_kind_of_term flags env evd term1 sk1,
+         flex_kind_of_term flags env evd term2 sk2) with
+    | Flexible (sp1,al1), Flexible (sp2,al2) ->
         (* sk1[?ev1] =? sk2[?ev2] *)
-	let f1 i =
-          (* Try first-order unification *)
-	  match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
-	  | None, Success i' ->
-            (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
-            (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
-	    let ev1' = whd_evar i' (mkEvar ev1) in
-	      if isEvar i' ev1' then
-		solve_simple_eqn (evar_conv_x ts) env i'
-		  (position_problem true pbty,destEvar i' ev1', term2)
-	      else 
-		evar_eqappr_x ts env evd pbty 
-		  ((ev1', sk1), csts1) ((term2, sk2), csts2)
-	  | Some (r,[]), Success i' ->
-            (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
-            (* we now unify r[?ev1] and ?ev2 *)
-	    let ev2' = whd_evar i' (mkEvar ev2) in
-	      if isEvar i' ev2' then
-		solve_simple_eqn (evar_conv_x ts) env i'
-		  (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r))
-	      else 
-		evar_eqappr_x ts env evd pbty 
-		  ((ev2', sk1), csts1) ((term2, sk2), csts2)
-	  | Some ([],r), Success i' ->
-            (* Symmetrically *)
-            (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
-            (* we now unify ?ev1 and r[?ev2] *)
-	    let ev1' = whd_evar i' (mkEvar ev1) in
-	      if isEvar i' ev1' then
-		solve_simple_eqn (evar_conv_x ts) env i'
-	          (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r))
-	      else evar_eqappr_x ts env evd pbty 
-		((ev1', sk1), csts1) ((term2, sk2), csts2)
-	  | None, (UnifFailure _ as x) ->
-             (* sk1 and sk2 have no common outer part *)
-             if Stack.not_purely_applicative sk2 then
-               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
-               flex_rigid true ev1 appr1 appr2
-             else
-             if Stack.not_purely_applicative sk1 then
-               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
-               flex_rigid false ev2 appr2 appr1
-             else
-               (* We could instead try Miller unification, then
-                  postpone to see if other equations help, as in:
-                  [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *)
-               x
-	  | Some _, Success _ ->
-             (* sk1 and sk2 have a common outer part *)
-             if Stack.not_purely_applicative sk2 then
-               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
-               flex_rigid true ev1 appr1 appr2
-             else
-             if Stack.not_purely_applicative sk1 then
-               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
-               flex_rigid false ev2 appr2 appr1
-             else
-               (* We could instead try Miller unification, then
-                  postpone to see if other equations help, as in:
-                  [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *)
-               UnifFailure (i,NotSameArgSize)
-          | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")
-
+        let f1 i = first_order env i term1 term2 sk1 sk2
 	and f2 i =
           if Evar.equal sp1 sp2 then
-	    match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
+            match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
 	    |None, Success i' ->
-              Success (solve_refl (fun env i pbty a1 a2 ->
-                is_success (evar_conv_x ts 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)) flags
                 env i' (position_problem true pbty) sp1 al1 al2)
 	    |_, (UnifFailure _ as x) -> x
             |Some _, _ -> UnifFailure (i,NotSameArgSize)
           else UnifFailure (i,NotSameHead)
-	in
-	ise_try evd [f1; f2]
+        and f3 i = miller true (sp1,al1) appr1 appr2 i
+        and f4 i = miller false (sp2,al2) appr2 appr1 i
+        and f5 i =
+          (* We ensure failure of consuming the stacks does not
+             propagate an error about unification of the stacks while
+             the heads themselves cannot be unified, so we return
+             NotSameHead. *)
+          match consume true appr1 appr2 i with
+          | Success _ as x -> x
+          | UnifFailure _ -> quick_fail i
+        in
+        ise_try evd [f1; f2; f3; f4; f5]
 
     | Flexible ev1, MaybeFlexible v2 ->
       flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2
@@ -687,31 +809,31 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         let f1 i = (* FO *)
           ise_and i
             [(fun i -> ise_try i
-               [(fun i -> evar_conv_x ts env i CUMUL t1 t2);
-                (fun i -> evar_conv_x ts env i CUMUL t2 t1)]);
-             (fun i -> evar_conv_x ts env i CONV b1 b2);
+               [(fun i -> evar_conv_x flags env i CUMUL t1 t2);
+                (fun i -> evar_conv_x flags env i CUMUL t2 t1)]);
+             (fun i -> evar_conv_x flags env i CONV b1 b2);
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
                let na = Nameops.Name.pick na1 na2 in
-	       evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
-	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+               evar_conv_x flags (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
+             (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
 	and f2 i =
-          let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
-          and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
-	  in evar_eqappr_x ts env i pbty out1 out2
+          let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1)
+          and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2)
+          in evar_eqappr_x flags env i pbty out1 out2
 	in
 	ise_try evd [f1; f2]
 
         | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' ->
 	  let f1 i = 
 	    ise_and i 
-	    [(fun i -> evar_conv_x ts env i CONV c c');
-	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+            [(fun i -> evar_conv_x flags env i CONV c c');
+             (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
 	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
-            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
-	    in evar_eqappr_x ts env i pbty out1 out2
+            let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1)
+            and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2)
+            in evar_eqappr_x flags env i pbty out1 out2
 	  in
 	    ise_try evd [f1; f2]
 	      
@@ -723,7 +845,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  in
 	    (match res with 
 	    | Some (f1,args1) -> 
-	      evar_eqappr_x ts env evd pbty ((f1,Stack.append_app args1 sk1),csts1) 
+              evar_eqappr_x flags env evd pbty ((f1,Stack.append_app args1 sk1),csts1)
 		(appr2,csts2)
 	    | None -> UnifFailure (evd,NotSameHead))
 	      
@@ -734,7 +856,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  in 
 	    (match res with
 	    | Some (f2,args2) ->
-	      evar_eqappr_x ts env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2)
+              evar_eqappr_x flags env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2)
 	    | None -> UnifFailure (evd,NotSameHead))
 	      
 	| _, _ ->
@@ -751,13 +873,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		try Success (Evd.add_universe_constraints i univs)
 		with UniversesDiffer -> UnifFailure (i,NotSameHead)
 		| Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-			 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+                         (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
           | None ->
             UnifFailure (i,NotSameHead)
 	and f2 i =
 	  (try 
-	     if not (snd ts) then raise Not_found
-	     else conv_record ts env i
+             if not flags.with_cs then raise Not_found
+             else conv_record flags env i
                (try check_conv_record env i appr1 appr2
 		with Not_found -> check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
@@ -775,7 +897,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             | Lambda _ -> assert (match args with [] -> true | _ -> false); true
             | LetIn (_,b,_,c) -> is_unnamed
 	     (fst (whd_betaiota_deltazeta_for_iota_state
-		      (fst ts) env i Cst_stack.empty (subst1 b c, args)))
+                      flags.open_ts env i Cst_stack.empty (subst1 b c, args)))
 	    | Fix _ -> true (* Partially applied fix can be the result of a whd call *)
 	    | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args
             | Case _ | App _| Cast _ -> assert false in
@@ -783,20 +905,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    let applicative_stack = fst (Stack.strip_app sk2) in
 	    is_unnamed
 	      (fst (whd_betaiota_deltazeta_for_iota_state
-		      (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in
+                      flags.open_ts env i Cst_stack.empty (v2, applicative_stack))) in
           let rhs_is_already_stuck =
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
 
 	  if (EConstr.isLambda i term1 || rhs_is_already_stuck)
 	    && (not (Stack.not_purely_applicative sk1)) then
-	    evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
+            evar_eqappr_x ~rhs_is_already_stuck flags env i pbty
 	      (whd_betaiota_deltazeta_for_iota_state
-		 (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+                 flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
 	      (appr2,csts2)
 	  else
-	    evar_eqappr_x ts env i pbty (appr1,csts1)
+            evar_eqappr_x flags env i pbty (appr1,csts1)
 	      (whd_betaiota_deltazeta_for_iota_state
-		 (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+                 flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 	in
 	ise_try evd [f1; f2; f3]
     end
@@ -804,13 +926,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 ->
         let (na1,c1,c'1) = EConstr.destLambda evd term1 in
         let (na2,c2,c'2) = EConstr.destLambda evd term2 in
-        assert app_empty;
         ise_and evd
-          [(fun i -> evar_conv_x ts env i CONV c1 c2);
+          [(fun i -> evar_conv_x flags env i CONV c1 c2);
            (fun i ->
 	     let c = nf_evar i c1 in
              let na = Nameops.Name.pick na1 na2 in
-	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
+             evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2);
+           (* When in modulo_betaiota = false case, lambda's are not reduced *)
+           (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
     | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
@@ -818,13 +941,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | MaybeFlexible v1, Rigid ->
 	let f3 i =
 	  (try 
-	     if not (snd ts) then raise Not_found
-	     else conv_record ts env i (check_conv_record env i appr1 appr2)
+             if not flags.with_cs then raise Not_found
+             else conv_record flags env i (check_conv_record env i appr1 appr2)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
-	  evar_eqappr_x ts env i pbty
+          evar_eqappr_x flags env i pbty
 	    (whd_betaiota_deltazeta_for_iota_state
-	       (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+               flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
 	    (appr2,csts2)
 	in
 	  ise_try evd [f3; f4]
@@ -832,13 +955,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | Rigid, MaybeFlexible v2 ->
 	let f3 i =
 	  (try
-	     if not (snd ts) then raise Not_found
-	     else conv_record ts env i (check_conv_record env i appr2 appr1)
+             if not flags.with_cs then raise Not_found
+             else conv_record flags env i (check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
-	  evar_eqappr_x ts env i pbty (appr1,csts1)
+          evar_eqappr_x flags env i pbty (appr1,csts1)
 	    (whd_betaiota_deltazeta_for_iota_state
-	       (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+               flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 	in
 	  ise_try evd [f3; f4]
 
@@ -867,20 +990,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
 	| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
             ise_and evd
-              [(fun i -> evar_conv_x ts env i CONV c1 c2);
+              [(fun i -> evar_conv_x flags env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
                  let na = Nameops.Name.pick n1 n2 in
-	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
+                 evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
 	    if Int.equal x1 x2 then
-              exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
+              exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2
             else UnifFailure (evd,NotSameHead)
 
 	| Var var1, Var var2 ->
 	    if Id.equal var1 var2 then
-              exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
+              exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2
             else UnifFailure (evd,NotSameHead)
 
 	| Const _, Const _
@@ -889,49 +1012,59 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         | Int _, Int _ ->
           rigids env evd sk1 term1 sk2 term2
 
+        | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *)
+          if Evar.equal sp1 sp2 then
+            match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with
+            |None, Success i' ->
+              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)
+
 	| Construct u, _ ->
-	  eta_constructor ts env evd sk1 u sk2 term2
+          eta_constructor flags env evd sk1 u sk2 term2
 	    
 	| _, Construct u ->
-	  eta_constructor ts env evd sk2 u sk1 term1
+          eta_constructor flags env evd sk2 u sk1 term1
 
 	| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
 	  if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
             ise_and evd [
-	      (fun i -> ise_array2 i (fun i' -> evar_conv_x ts env i' CONV) tys1 tys2);
-	      (fun i -> ise_array2 i (fun i' -> evar_conv_x ts (push_rec_types recdef1 env) i' CONV) bds1 bds2);
-	      (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+              (fun i -> ise_array2 i (fun i' -> evar_conv_x flags env i' CONV) tys1 tys2);
+              (fun i -> ise_array2 i (fun i' -> evar_conv_x flags (push_rec_types recdef1 env) i' CONV) bds1 bds2);
+              (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
 	  else UnifFailure (evd, NotSameHead)
 
 	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
             if Int.equal i1 i2  then
               ise_and evd
                 [(fun i -> ise_array2 i
-                    (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
+                    (fun i -> evar_conv_x flags env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
-		     (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
+                     (fun i -> evar_conv_x flags (push_rec_types recdef1 env) i CONV)
 		     bds1 bds2);
                  (fun i -> exact_ise_stack2 env i
-                     (evar_conv_x ts) sk1 sk2)]
+                     (evar_conv_x flags) sk1 sk2)]
             else UnifFailure (evd,NotSameHead)
 
 	| (Meta _, _) | (_, Meta _) ->
-	  begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with
+          begin match ise_stack2 true env evd (evar_conv_x flags) sk1 sk2 with
 	  |_, (UnifFailure _ as x) -> x
-	  |None, Success i' -> evar_conv_x ts env i' CONV term1 term2
-	  |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
+          |None, Success i' -> evar_conv_x flags env i' CONV term1 term2
+          |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
 	  end
 
-        | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _), _ ->
+        | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _), _ ->
 	  UnifFailure (evd,NotSameHead)
-
-	| (App _ | Cast _ | Case _ | Proj _), _ -> assert false
-	| (LetIn _| Evar _), _ -> assert false
-	| (Lambda _), _ -> assert false
-
+        | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) ->
+          UnifFailure (evd,NotSameHead)
+        | Case _, _ -> UnifFailure (evd,NotSameHead)
+        | Proj _, _ -> UnifFailure (evd,NotSameHead)
+        | (App _ | Cast _), _ -> assert false
+        | LetIn _, _ -> assert false
       end
 
-and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
+and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
   (* Tries to unify the states
 
         (proji params1 c1 | sk1)   =   (proji params2 (c (?xs:bs)) | sk2)
@@ -962,7 +1095,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 	(fun (i,ks,m,test) b ->
 	  if match n with Some n -> Int.equal m n | None -> false then
 	    let ty = Retyping.get_type_of env i t2 in
-	    let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
+            let test i = evar_conv_x flags env i CUMUL ty (substl ks b) in
 	      (i,t2::ks, m-1, test)
 	  else
 	    let dloc = Loc.tag Evar_kinds.InternalHole in
@@ -974,20 +1107,20 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
     ise_and evd'
       [(fun i ->
 	exact_ise_stack2 env i
-          (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x))
+          (fun env' i' cpb x1 x -> evar_conv_x flags env' i' cpb x1 (substl ks x))
           params1 params);
        (fun i ->
 	 exact_ise_stack2 env i
-           (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u))
+           (fun env' i' cpb u1 u -> evar_conv_x flags env' i' cpb u1 (substl ks u))
            us2 us);
-       (fun i -> evar_conv_x trs env i CONV c1 app);
-       (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
+       (fun i -> evar_conv_x flags env i CONV c1 app);
+       (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2);
        test;
-       (fun i -> evar_conv_x trs env i CONV h2
+       (fun i -> evar_conv_x flags env i CONV h2
 	 (fst (decompose_app_vect i (substl ks h))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
-and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
+and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 =
   let open Declarations in
   let mib = lookup_mind (fst ind) env in
     match get_projections env ind with
@@ -999,15 +1132,17 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
 	     let term = Stack.zip evd (term2,sk2) in 
 	       List.map (fun p -> EConstr.mkProj (Projection.make p false, term)) (Array.to_list projs)
 	   in
-	     exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' 
+             exact_ise_stack2 env evd (evar_conv_x { flags with with_cs = false}) l1'
 	       (Stack.append_app_list l2' Stack.empty)
-	 with 
+         with
 	 | Invalid_argument _ ->
 	   (* Stack.tail: partially applied constructor *)
 	   UnifFailure(evd,NotSameHead))
     | _ -> UnifFailure (evd,NotSameHead)
 
-let evar_conv_x ts = evar_conv_x (ts, true)
+let evar_conv_x flags = evar_conv_x flags
+
+let evar_unify = conv_fun evar_conv_x
 
 (* Profiling *)
 let evar_conv_x =
@@ -1018,25 +1153,26 @@ let evar_conv_x =
 
 let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x ()
 
-let evar_conv_x ts = Hook.get evar_conv_hook_get ts
+let evar_conv_x flags = Hook.get evar_conv_hook_get flags
 
 let set_evar_conv f = Hook.set evar_conv_hook_set f
 
 
 (* We assume here |l1| <= |l2| *)
 
-let first_order_unification ts env evd (ev1,l1) (term2,l2) =
+let first_order_unification flags env evd (ev1,l1) (term2,l2) =
   let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in
   ise_and evd
     (* First compare extra args for better failure message *)
-    [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
+    [(fun i -> ise_array2 i (fun i -> evar_conv_x flags env i CONV) rest2 l1);
     (fun i ->
       (* Then instantiate evar unless already done by unifying args *)
       let t2 = mkApp(term2,deb2) in
       if is_defined i (fst ev1) then
-	evar_conv_x ts env i CONV t2 (mkEvar ev1)
+        evar_conv_x flags env i CONV t2 (mkEvar ev1)
       else
-	solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))]
+        solve_simple_eqn ~choose:true ~imitate_defs:false
+          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
@@ -1046,30 +1182,57 @@ let choose_less_dependent_instance evk evd term args =
   | [] -> None
   | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
 
-let apply_on_subterm env evdref f c t =
+type occurrence_match_test =
+  env -> evar_map -> constr ->
+  env -> evar_map -> int -> constr -> constr -> bool * evar_map
+
+type occurrence_selection =
+  | AtOccurrences of Locus.occurrences
+  | Unspecified of Abstraction.abstraction
+
+type occurrences_selection =
+  occurrence_match_test * occurrence_selection list
+
+let default_occurrence_selection = Unspecified Abstraction.Imitate
+
+let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat =
+  let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in
+  match evar_conv_x flags env sigma CONV c pat with
+  | Success sigma -> true, sigma
+  | UnifFailure _ -> false, sigma
+
+let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n =
+  (default_occurrence_test ~frozen_evars ts,
+   List.init n (fun _ -> default_occurrence_selection))
+
+let apply_on_subterm env evd fixedref f test c t =
+  let test = test env evd c in
+  let prc env evd = Termops.Internal.print_constr_env env evd in
+  let evdref = ref evd in
   let rec applyrec (env,(k,c) as acc) t =
-    (* By using eq_constr, we make an approximation, for instance, we *)
-    (* could also be interested in finding a term u convertible to t *)
-    (* such that c occurs in u *)
-    let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
-    | None -> false
-    | Some cstr ->
-      try ignore (Evd.add_universe_constraints !evdref cstr); true
-      with UniversesDiffer -> false
-    in
-    if eq_constr c t then f k
-    else
+    if Evar.Set.exists (fun fixed -> occur_evar !evdref fixed t) !fixedref then
       match EConstr.kind !evdref t with
-      | Evar (evk,args) ->
-          let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
-          let g decl a = if is_local_assum decl then applyrec acc a else a in
-          mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
-      | _ ->
-        map_constr_with_binders_left_to_right !evdref
-	  (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
-	  applyrec acc t
+      | Evar (ev, args) when Evar.Set.mem ev !fixedref -> t
+      | _ -> map_constr_with_binders_left_to_right !evdref
+              (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
+              applyrec acc t
+    else
+    (if !debug_ho_unification then
+     Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t);
+     let b, evd =
+        try test env !evdref k c t
+        with e when CErrors.noncritical e -> assert false in
+     if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded");
+                let evd', t' = f !evdref k t in
+                evdref := evd'; t')
+     else (
+       if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed");
+       map_constr_with_binders_left_to_right !evdref
+        (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
+        applyrec acc t))
   in
-  applyrec (env,(0,c)) t
+  let t' = applyrec (env,(0,c)) t in
+  !evdref, t'
 
 let filter_possible_projections evd c ty ctxt args =
   (* Since args in the types will be replaced by holes, we count the
@@ -1114,117 +1277,283 @@ let set_solve_evars f = solve_evars := f
  * proposition from Dan Grayson]
  *)
 
+let check_selected_occs env sigma c occ occs =
+  let notfound =
+    match occs with
+    | AtOccurrences occs ->
+       (match occs with
+       | Locus.AtLeastOneOccurrence -> occ == 1
+       | Locus.AllOccurrences -> false
+       | Locus.AllOccurrencesBut l -> List.last l > occ
+       | Locus.OnlyOccurrences l -> List.last l > occ
+       | Locus.NoOccurrences -> false)
+    | Unspecified abstract -> false
+  in if notfound then
+     raise (PretypeError (env,sigma,NoOccurrenceFound (c,None)))
+     else ()
+
 exception TypingFailed of evar_map
 
-let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
+let set_of_evctx l =
+  List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l
+
+(** Weaken the existentials so that they can be typed in sign and raise
+    an error if the term otherwise mentions variables not bound in sign. *)
+let thin_evars env sigma sign c =
+  let evdref = ref sigma in
+  let ctx = set_of_evctx sign in
+  let rec applyrec (env,acc) t =
+    match kind sigma t with
+    | Evar (ev, args) ->
+       let evi = Evd.find_undefined sigma ev in
+       let filter = Array.map (fun c -> Id.Set.subset (collect_vars sigma c) ctx) args in
+       let filter = Filter.make (Array.to_list filter) in
+       let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in
+       let evd, ev = restrict_evar !evdref ev filter candidates in
+       evdref := evd; whd_evar !evdref t
+    | Var id ->
+       if not (Id.Set.mem id ctx) then raise (TypingFailed sigma)
+       else t
+    | _ ->
+       map_constr_with_binders_left_to_right !evdref
+        (fun d (env,acc) -> (push_rel d env, acc+1))
+        applyrec (env,acc) t
+  in
+  let c' = applyrec (env,0) c in
+  (!evdref, c')
+
+let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   try
   let evi = Evd.find_undefined evd evk in
+  let evi = nf_evar_info evd evi in
+  let env_evar_unf = evar_env evi in
   let env_evar = evar_filtered_env evi in
   let sign = named_context_val env_evar in
   let ctxt = evar_filtered_context evi in
-  let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in
-
+  if !debug_ho_unification then
+    (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
+     Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
+  let args = Array.map (nf_evar evd) args in
+  let vars = List.map NamedDecl.get_id ctxt in
+  let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in
+  let instance = List.map mkVar vars in
+  let rhs = nf_evar evd rhs in
+  if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd);
+  (* Ensure that any progress made by Typing.e_solve_evars will not contradict
+      the solution we are trying to build here by adding the problem as a constraint. *)
+  let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkEvar (evk,args),rhs) evd in
+  let prc env evd c = Termops.Internal.print_constr_env env evd c in
   let rec make_subst = function
-  | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c ->
+    | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c ->
       begin match occs with
-      | Some _ ->
-        user_err Pp.(str "Cannot force abstraction on identity instance.")
-      | None ->
-        make_subst (ctxt',l,occsl)
+        | AtOccurrences loc when not (Locusops.is_all_occurrences loc) ->
+          user_err Pp.(str "Cannot force abstraction on identity instance.")
+        | _ ->
+          make_subst (ctxt',l,occsl)
       end
-  | decl'::ctxt', c::l, occs::occsl ->
+    | decl'::ctxt', c::l, occs::occsl ->
       let id = NamedDecl.get_id decl' in
       let t = NamedDecl.get_type decl' in
       let evs = ref [] in
-      let ty = Retyping.get_type_of env_rhs evd c in
-      let filter' = filter_possible_projections evd c ty ctxt args in
+      let c = nf_evar evd c in
+      (* ty is in env_rhs now *)
+      let ty = replace_vars argsubst t in
+      let filter' = filter_possible_projections evd c (nf_evar evd ty) ctxt args in
       (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
-  | _, _, [] -> []
-  | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in
-
-  let rec set_holes evdref rhs = function
-  | (id,_,c,cty,evsref,filter,occs)::subst ->
-      let set_var k =
-        match occs with
-        | Some Locus.AllOccurrences -> mkVar id
-        | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported")
-        | None ->
-        let evty = set_holes evdref cty subst in
-        let instance = Filter.filter_list filter instance in
-        let evd = !evdref in
-        let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
-        evdref := evd;
-        evsref := (fst (destEvar !evdref ev),evty)::!evsref;
-        ev in
-      set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
-  | [] -> rhs in
+    | _, _, [] -> []
+    | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.")
+  in
+  let fixed = ref Evar.Set.empty in
+  let rec set_holes env_rhs evd rhs = function
+  | (id,idty,c,cty,evsref,filter,occs)::subst ->
+     let c = nf_evar evd c in
+     if !debug_ho_unification then
+       Feedback.msg_debug Pp.(str"set holes for: " ++
+                                prc env_rhs evd (mkVar id) ++ spc () ++
+                                prc env_rhs evd c ++ str" in " ++
+                                prc env_rhs evd rhs);
+     let occ = ref 1 in
+     let set_var evd k inst =
+       let oc = !occ in
+       if !debug_ho_unification then
+       (Feedback.msg_debug Pp.(str"Found one occurrence");
+        Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c));
+       incr occ;
+       match occs with
+       | AtOccurrences occs ->
+          if Locusops.is_selected oc occs then evd, mkVar id
+          else evd, inst
+       | Unspecified prefer_abstraction ->
+          let evd, evty = set_holes env_rhs evd cty subst in
+          let evty = nf_evar evd evty in
+          if !debug_ho_unification then
+            Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
+                                   str" of type: " ++ prc env_evar evd evty ++
+                                   str " for " ++ prc env_rhs evd c);
+          let instance = Filter.filter_list filter instance in
+          (* Allow any type lower than the variable's type as the
+             abstracted subterm might have a smaller type, which could be
+             crucial to make the surrounding context typecheck. *)
+          let evd, evty =
+            if isArity evd evty then
+              refresh_universes ~status:Evd.univ_flexible (Some true)
+                env_evar_unf evd evty
+            else evd, evty in
+          let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
+          let evk = fst (destEvar evd ev) in
+          evsref := (evk,evty,inst,prefer_abstraction)::!evsref;
+          fixed := Evar.Set.add evk !fixed;
+          evd, ev
+     in
+     let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
+     if !debug_ho_unification then
+       Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs');
+     let () = check_selected_occs env_rhs evd c !occ occs in
+     let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
+     set_holes env_rhs' evd rhs' subst
+  | [] -> evd, rhs in
 
   let subst = make_subst (ctxt,Array.to_list args,argoccs) in
 
-  let evd, rhs =
-    let evdref = ref evd in
-    let rhs = set_holes evdref rhs subst in
-    !evdref, rhs
-  in
-
+  let evd, rhs' = set_holes env_rhs evd rhs subst in
+  let rhs' = nf_evar evd rhs' in
+  (* Thin evars making the term typable in env_evar *)
+  let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
-  let evd,rhs =
-    try !solve_evars env_evar evd rhs
+  if !debug_ho_unification then
+    (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs');
+     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
+  let evd,rhs' =
+    try !solve_evars env_evar evd rhs'
     with e when Pretype_errors.precatchable_exception e ->
       (* Could not revert all subterms *)
       raise (TypingFailed evd) in
+  let rhs' = nf_evar evd rhs' in
+  (* We instantiate the evars of which the value is forced by typing *)
+  if !debug_ho_unification then
+    (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs');
+     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
 
   let rec abstract_free_holes evd = function
-  | (id,idty,c,_,evsref,_,_)::l ->
-      let rec force_instantiation evd = function
-      | (evk,evty)::evs ->
-          let evd =
-            if is_undefined evd evk then
-              (* We force abstraction over this unconstrained occurrence *)
-              (* and we use typing to propagate this instantiation *)
-              (* This is an arbitrary choice *)
-              let evd = Evd.define evk (mkVar id) evd in
-              match evar_conv_x ts env_evar evd CUMUL idty evty with
-              | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
-              | Success evd ->
-              match reconsider_unif_constraints (evar_conv_x ts) evd with
-              | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
-              | Success evd ->
-              evd
-            else
-              evd
-          in
-          force_instantiation evd evs
-      | [] ->
-          abstract_free_holes evd l
-      in
-      force_instantiation evd !evsref
-  | [] ->
-    let evd = 
-      try Evarsolve.check_evar_instance evd evk rhs
-            (evar_conv_x TransparentState.full)
-      with IllTypedInstance _ -> raise (TypingFailed evd)
-    in
-      Evd.define evk rhs evd
+   | (id,idty,c,cty,evsref,_,_)::l ->
+     let c = nf_evar evd c in
+     if !debug_ho_unification then
+       Feedback.msg_debug Pp.(str"abstracting: " ++
+                                prc env_rhs evd (mkVar id) ++ spc () ++
+                                prc env_rhs evd c);
+     let rec force_instantiation evd = function
+     | (evk,evty,inst,abstract)::evs ->
+       let evk = Option.default evk (Evarutil.advance evd evk) in
+       let evd =
+         if is_undefined evd evk then
+         (* We try abstraction or concretisation for *)
+         (* this unconstrained occurrence *)
+         (* and we use typing to propagate this instantiation *)
+         (* We avoid making an arbitrary choice by leaving candidates *)
+         (* if both can work *)
+         let evi = Evd.find_undefined evd evk in
+         let vid = mkVar id in
+         let candidates = [inst; vid] in
+           try
+             let evd, ev = Evarutil.restrict_evar evd evk (Evd.evar_filter evi) (Some candidates) in
+             let evi = Evd.find evd ev in
+               (match evar_candidates evi with
+               | Some [t] ->
+                 if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then
+                   raise (TypingFailed evd);
+                 instantiate_evar 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 ->
+                 instantiate_evar evar_unify flags evd ev vid
+               | _ -> evd)
+           with e -> user_err (Pp.str "Cannot find an instance")
+         else
+           ((if !debug_ho_unification then
+               let evi = Evd.find evd evk in
+               let env = Evd.evar_env evi in
+               Feedback.msg_debug Pp.(str"evar is defined: " ++
+                 int (Evar.repr evk) ++ spc () ++
+                 prc env evd (match evar_body evi with Evar_defined c -> c
+                   | Evar_empty -> assert false)));
+            evd)
+       in force_instantiation evd evs
+     | [] -> abstract_free_holes evd l
+     in force_instantiation evd !evsref
+   | [] ->
+     if Evd.is_defined evd evk then
+       (* Can happen due to dependencies: instantiating evars in the arguments of evk might
+           instantiate evk itself. *)
+       (if !debug_ho_unification then
+          begin
+            let evi = Evd.find evd evk in
+            let evenv = evar_env evi in
+            let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in
+            Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body)
+          end;
+        evd)
+     else
+       try
+         let evi = Evd.find_undefined evd evk in
+         let evenv = evar_env evi in
+         let rhs' = nf_evar evd rhs' in
+           if !debug_ho_unification then
+             Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
+                                      prc evenv evd rhs');
+         (* solve_evars is not commuting with nf_evar, because restricting
+             an evar might provide a more specific type. *)
+          let evd, _ = !solve_evars evenv evd rhs' in
+          if !debug_ho_unification then
+            Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'));
+          let flags = default_flags_of TransparentState.full in
+            Evarsolve.instantiate_evar evar_unify flags evd evk rhs'
+         with IllTypedInstance _ -> raise (TypingFailed evd)
   in
-  abstract_free_holes evd subst, true
+  let evd = abstract_free_holes evd subst in
+  evd, true
   with TypingFailed evd -> evd, false
 
-let second_order_matching_with_args ts env evd pbty ev l t =
-(*
-  let evd,ev = evar_absorb_arguments env evd ev l in
-  let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
-  let evd, b = second_order_matching ts env evd ev argoccs t in
-  if b then Success evd
-  else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
-  if b then Success evd else
- *)
-  let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
-  UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
-
-let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
-  let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
-  let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
+let default_evar_selection flags evd (ev,args) =
+  let evi = Evd.find_undefined evd ev in
+  let rec aux args abs =
+    match args, abs with
+    | _ :: args, a :: abs ->
+      let spec =
+        if not flags.allow_K_at_toplevel then
+          (* [evar_absorb_arguments] puts an Abstract flag for the
+             toplevel binders that were absorbed. *)
+          let occs =
+            if a == Abstraction.Abstract then Locus.AtLeastOneOccurrence
+            else Locus.AllOccurrences
+          in AtOccurrences occs
+        else Unspecified a
+      in spec :: aux args abs
+    | l, [] -> List.map (fun _ -> default_occurrence_selection) l
+    | [], _ :: _ -> assert false
+  in aux (Array.to_list args) evi.evar_abstract_arguments
+
+let second_order_matching_with_args flags env evd with_ho pbty ev l t =
+  if with_ho then
+    let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in
+    let argoccs = default_evar_selection flags evd ev in
+    let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in
+    let evd, b =
+      try second_order_matching flags env evd ev (test,argoccs) t
+      with PretypeError (_, _, NoOccurrenceFound _) -> evd, false
+    in
+    if b then Success evd
+    else
+      UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
+  else
+    let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
+    UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
+
+let is_beyond_capabilities = function
+  | CannotSolveConstraint (pb,ProblemBeyondCapabilities) -> true
+  | _ -> false
+
+let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
+  let t1 = apprec_nohdbeta flags env evd (whd_head_evar evd t1) in
+  let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
   let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
   let () = if !debug_unification then
@@ -1234,7 +1563,8 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
                                 Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
   match EConstr.kind evd term1, EConstr.kind evd term2 with
-  | Evar (evk1,args1), (Rel _|Var _) when app_empty
+  | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty
+      && not (is_frozen flags ev1)
       && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a)
         (remove_instance_local_defs evd evk1 args1) ->
       (* The typical kind of constraint coming from pattern-matching return
@@ -1244,8 +1574,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       | None ->
          let reason = ProblemBeyondCapabilities in
          UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
-  | (Rel _|Var _), Evar (evk2,args2) when app_empty
-      && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
+  | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty
+    && not (is_frozen flags ev2)
+    && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
         (remove_instance_local_defs evd evk2 args2) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
@@ -1255,36 +1586,44 @@ let apply_conversion_problem_heuristic ts env evd 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 env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
-      Success (solve_refl ~can_drop:true f env evd
+     let f flags ontype env evd pbty x y =
+       let reds =
+         match ontype with
+         | TypeUnification -> TransparentState.full
+         | TermUnification -> flags.open_ts
+       in is_fconv ~reds pbty env evd x y
+     in
+      Success (solve_refl ~can_drop:true f flags env evd
                  (position_problem true pbty) evk1 args1 args2)
   | Evar ev1, Evar ev2 when app_empty ->
+    (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *)
       Success (solve_evar_evar ~force:true
-        (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 ->
+                 (evar_define evar_unify flags ~choose:true)
+                 evar_unify flags env evd
+                 (position_problem true pbty) ev1 ev2)
+  | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       (* and otherwise second-order matching *)
       ise_try evd
-        [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2);
+        [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2);
          (fun evd ->
-           second_order_matching_with_args ts env evd pbty ev1 l1 t2)]
-  | _,Evar ev2 when Array.length l2 <= Array.length l1 ->
+           second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)]
+  | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 ->
       (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
       (* and otherwise second-order matching *)
       ise_try evd
-        [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1);
+        [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1);
          (fun evd ->
-           second_order_matching_with_args ts env evd pbty ev2 l2 t1)]
-  | Evar ev1,_ ->
+           second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)]
+  | Evar ev1,_ when not (is_frozen flags ev1) ->
       (* Try second-order pattern-matching *)
-      second_order_matching_with_args ts env evd pbty ev1 l1 t2
-  | _,Evar ev2 ->
+      second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2
+  | _,Evar ev2 when not (is_frozen flags ev2) ->
       (* Try second-order pattern-matching *)
-      second_order_matching_with_args ts env evd pbty ev2 l2 t1
+      second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1
   | _ ->
       (* Some head evar have been instantiated, or unknown kind of problem *)
-      evar_conv_x ts env evd pbty t1 t2
+      evar_conv_x flags env evd pbty t1 t2
 
 let error_cannot_unify env evd pb ?reason t1 t2 =
   Pretype_errors.error_cannot_unify
@@ -1313,7 +1652,7 @@ let max_undefined_with_candidates evd =
   with MaxUndefined ans ->
     Some ans
 
-let rec solve_unconstrained_evars_with_candidates ts evd =
+let rec solve_unconstrained_evars_with_candidates flags evd =
   (* max_undefined is supposed to return the most recent, hence
      possibly most dependent evar *)
   match max_undefined_with_candidates evd with
@@ -1324,11 +1663,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
       | a::l ->
           (* In case of variables, most recent ones come first *)
           try
-            let conv_algo = evar_conv_x ts in
-            let evd = check_evar_instance evd evk a conv_algo in
-            let evd = Evd.define evk a evd in
-            match reconsider_unif_constraints conv_algo evd with
-            | Success evd -> solve_unconstrained_evars_with_candidates ts evd
+            let evd = instantiate_evar evar_unify flags evd evk a in
+            match reconsider_unif_constraints evar_unify flags evd with
+            | Success evd -> solve_unconstrained_evars_with_candidates flags evd
             | UnifFailure _ -> aux l
           with
           | IllTypedInstance _ -> aux l
@@ -1336,7 +1673,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
       (* Expected invariant: most dependent solutions come first *)
       (* so as to favor progress when used with the refine tactics *)
       let evd = aux l in
-      solve_unconstrained_evars_with_candidates ts evd
+      solve_unconstrained_evars_with_candidates flags evd
 
 let solve_unconstrained_impossible_cases env evd =
   Evd.fold_undefined (fun evk ev_info evd' ->
@@ -1345,35 +1682,40 @@ 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 = evar_conv_x TransparentState.full in
-      let evd' = check_evar_instance evd' evk ty conv_algo in
-        Evd.define evk ty evd'
+      let flags = default_flags env in
+      instantiate_evar evar_unify flags evd' evk ty
     | _ -> evd') evd evd
 
 let solve_unif_constraints_with_heuristics env
-    ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd =
-  let evd = solve_unconstrained_evars_with_candidates ts evd in
+    ?(flags=default_flags env) ?(with_ho=false) evd =
+  let evd = solve_unconstrained_evars_with_candidates flags evd in
   let rec aux evd pbs progress stuck =
     match pbs with
     | (pbty,env,t1,t2 as pb) :: pbs ->
-        (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
+        (match apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 with
 	| Success evd' ->
-	    let (evd', rest) = extract_all_conv_pbs evd' in
-            begin match rest with
+           let evd' = solve_unconstrained_evars_with_candidates flags evd' in
+           let (evd', rest) = extract_all_conv_pbs evd' in
+           begin match rest with
             | [] -> aux evd' pbs true stuck
-            | _ -> (* Unification got actually stuck, postpone *)
-	      aux evd pbs progress (pb :: stuck)
+            | l ->
+               (* Unification got actually stuck, postpone *)
+               let reason = CannotSolveConstraint (pb,ProblemBeyondCapabilities) in
+               aux evd pbs progress ((pb, reason):: stuck)
             end
         | UnifFailure (evd,reason) ->
-           error_cannot_unify env evd pb ~reason t1 t2)
+           if is_beyond_capabilities reason then
+             aux evd pbs progress ((pb,reason) :: stuck)
+           else aux evd [] false ((pb,reason) :: stuck))
     | _ -> 
-	if progress then aux evd stuck false []
+        if progress then aux evd (List.map fst stuck) false []
 	else 
 	  match stuck with
 	  | [] -> (* We're finished *) evd
-	  | (pbty,env,t1,t2 as pb) :: _ ->
-             (* There remains stuck problems *)
-             error_cannot_unify env evd pb t1 t2
+          | ((pbty,env,t1,t2 as pb), reason) :: _ ->
+              (* There remains stuck problems *)
+              Pretype_errors.error_cannot_unify ?loc:(loc_of_conv_pb evd pb)
+                env evd ~reason (t1, t2)
   in
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = aux evd pbs false [] in
@@ -1384,16 +1726,49 @@ let solve_unif_constraints_with_heuristics env
 
 exception UnableToUnify of evar_map * unification_error
 
-let default_transparent_state env = TransparentState.full
-(* Conv_oracle.get_transp_state (Environ.oracle env) *)
+let unify_delay ?flags env evd t1 t2 =
+  let flags =
+    match flags with
+    | None -> default_flags_of (default_transparent_state env)
+    | Some flags -> flags
+  in
+  match evar_conv_x flags env evd CONV t1 t2 with
+  | Success evd' -> evd'
+  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
+let unify_leq_delay ?flags env evd t1 t2 =
+  let flags =
+    match flags with
+    | None -> default_flags_of (default_transparent_state env)
+    | Some flags -> flags
+  in
+  match evar_conv_x flags env evd CUMUL t1 t2 with
+  | Success evd' -> evd'
+  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
+
+let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 =
+  let flags =
+    match flags with
+    | None -> default_flags_of (default_transparent_state env)
+    | Some flags -> flags
+  in
+  let res = evar_conv_x flags env evd cv_pb ty1 ty2 in
+  match res with
+  | Success evd ->
+     solve_unif_constraints_with_heuristics ~flags ~with_ho env evd
+  | UnifFailure (evd, reason) ->
+     raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason)))
+
+(* deprecated *)
 let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
-  match evar_conv_x ts env evd CONV  t1 t2 with
+  let flags = default_flags_of ts in
+  match evar_conv_x flags env evd CONV  t1 t2 with
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
 let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
-  match evar_conv_x ts env evd CUMUL t1 t2 with
+  let flags = default_flags_of ts in
+  match evar_conv_x flags env evd CUMUL t1 t2 with
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
@@ -1402,7 +1777,9 @@ let make_opt = function
   | UnifFailure _ -> None
 
 let conv env ?(ts=default_transparent_state env) evd t1 t2 =
-  make_opt(evar_conv_x ts env evd CONV t1 t2)
+  let flags = default_flags_of ts in
+  make_opt(evar_conv_x flags env evd CONV t1 t2)
 
 let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
-  make_opt(evar_conv_x ts env evd CUMUL t1 t2)
+  let flags = default_flags_of ts in
+  make_opt(evar_conv_x flags env evd CUMUL t1 t2)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 4585fac252..0fe47c2a48 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -16,28 +16,74 @@ open Locus
 
 (** {4 Unification for type inference. } *)
 
+type unify_flags = Evarsolve.unify_flags
+
+(** The default subterm transparent state is no unfoldings *)
+val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags
+
+type unify_fun = unify_flags ->
+  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
+
+val conv_fun : unify_fun -> Evarsolve.unifier
+
 exception UnableToUnify of evar_map * Pretype_errors.unification_error
 
 (** {6 Main unification algorithm for type inference. } *)
 
-(** returns exception NotUnifiable with best known evar_map if not unifiable *)
+(** There are two variants for unification: one that delays constraints outside its capabilities
+    ([unify_delay]) and another that tries to solve such remaining constraints using
+    heuristics ([unify]). *)
+
+(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints.
+    In case the flags are not specified, they default to
+    [default_flags_of TransparentState.full] currently.
+
+    In case of success, the two terms are hence unifiable only if the remaining constraints
+    can be solved or [check_problems_are_solved] is true.
+
+    @raises UnableToUnify in case the two terms do not unify *)
+
+val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
+val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
+
+(** returns exception UnableToUnify with best known evar_map if not unifiable *)
 val the_conv_x     : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
+[@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
 val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
-
+[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
 (** The same function resolving evars by side-effect and
    catching the exception *)
+
 val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
+[@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
 val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
+[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
+
+(** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining
+    constraints. In case of success the two terms are unified without condition.
+
+    The with_ho option tells if higher-order unification should be tried to resolve the
+    constraints.
+
+    @raises a PretypeError if it cannot unify *)
+val unify : ?flags:unify_flags -> ?with_ho:bool ->
+  env -> evar_map -> conv_pb -> constr -> constr -> evar_map
 
 (** {6 Unification heuristics. } *)
 
 (** Try heuristics to solve pending unification problems and to solve
-    evars with candidates *)
+   evars with candidates.
+
+   The with_ho option tells if higher-order unification should be tried
+   to resolve the constraints.
 
-val solve_unif_constraints_with_heuristics : env -> ?ts:TransparentState.t -> evar_map -> evar_map
+    @raises a PretypeError if it fails to resolve some problem *)
 
-(** Check all pending unification problems are solved and raise an
-    error otherwise *)
+val solve_unif_constraints_with_heuristics :
+  env -> ?flags:unify_flags -> ?with_ho:bool -> evar_map -> evar_map
+
+(** Check all pending unification problems are solved and raise a
+    PretypeError otherwise *)
 
 val check_problems_are_solved : env -> evar_map -> unit
 
@@ -54,28 +100,55 @@ val check_conv_record : env -> evar_map ->
 (** Try to solve problems of the form ?x[args] = c by second-order
     matching, using typing to select occurrences *)
 
-val second_order_matching : TransparentState.t -> env -> evar_map ->
-  EConstr.existential -> occurrences option list -> constr -> evar_map * bool
+type occurrence_match_test =
+  env -> evar_map -> constr -> (* Used to precompute the local tests *)
+  env -> evar_map -> int -> constr -> constr -> bool * evar_map
+
+(** When given the choice of abstracting an occurrence or leaving it,
+    force abstration. *)
+
+type occurrence_selection =
+  | AtOccurrences of occurrences
+  | Unspecified of Abstraction.abstraction
+
+(** By default, unspecified, not preferring abstraction.
+    This provides the most general solutions. *)
+val default_occurrence_selection : occurrence_selection
+
+type occurrences_selection =
+  occurrence_match_test * occurrence_selection list
+
+val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test
+
+(** [default_occurrence_selection n]
+    Gives the default test and occurrences for [n] arguments *)
+val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) ->
+  TransparentState.t -> int -> occurrences_selection
+
+val second_order_matching : unify_flags -> env -> evar_map ->
+  EConstr.existential -> occurrences_selection -> constr -> evar_map * bool
 
 (** Declare function to enforce evars resolution by using typing constraints *)
 
 val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
 
-type unify_fun = TransparentState.t ->
-  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
-
 (** Override default [evar_conv_x] algorithm. *)
 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 -> TransparentState.t * bool ->
+val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
   env -> evar_map ->
     conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
       Evarsolve.unification_result
+
+val occur_rigidly : Evarsolve.unify_flags ->
+  'a -> Evd.evar_map -> Evar.t * 'b -> EConstr.t -> bool
 (**/**)
 
 (** {6 Functions to deal with impossible cases } *)
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 571be7466c..a62427834d 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -139,7 +139,8 @@ let define_pure_evar_as_lambda env evd evk =
   let newenv = push_named (LocalAssum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = subterm_source evk ~where:Body (evar_source evk evd1) in
-  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+  let abstract_arguments = Abstraction.abstract_last evi.evar_abstract_arguments in
+  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter ~abstract_arguments in
   let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk lam evd2, lam
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4c4a236620..e5f2207333 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -24,6 +24,49 @@ open Reductionops
 open Evarutil
 open Pretype_errors
 
+type unify_flags = {
+  modulo_betaiota: bool;
+  open_ts : TransparentState.t;
+  closed_ts : TransparentState.t;
+  subterm_ts : TransparentState.t;
+  frozen_evars : Evar.Set.t;
+  allow_K_at_toplevel : bool;
+  with_cs : bool }
+
+type unification_kind =
+  | TypeUnification
+  | TermUnification
+
+(************************)
+(* Unification results  *)
+(************************)
+
+type unification_result =
+  | Success of evar_map
+  | UnifFailure of evar_map * unification_error
+
+let is_success = function Success _ -> true | UnifFailure _ -> false
+
+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 = unify_flags -> unification_kind ->
+  env ->  evar_map -> conv_pb -> constr -> constr -> bool
+
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
@@ -129,20 +172,6 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
     refresh_universes (Some false) env sigma ty
-		      
-
-(************************)
-(* Unification results  *)
-(************************)
-
-type unification_result =
-  | Success of evar_map
-  | UnifFailure of evar_map * unification_error
-
-let is_success = function Success _ -> true | UnifFailure _ -> false
-
-let test_success conv_algo env evd c c' rhs =
-  is_success (conv_algo env evd c c' rhs)
 
 let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
@@ -154,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) ->
@@ -165,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 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) ->
@@ -734,6 +763,19 @@ 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 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 *)
+  (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
+  let ty =
+    try Retyping.get_type_of ~lax:true evenv evd body
+    with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
+  in
+  match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
+  | Success evd -> evd
+  | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
+
 (***************)
 (* Unification *)
 
@@ -869,12 +911,13 @@ let rec find_solution_type evarenv = function
  * pass [define] to [do_projection_effects] as a parameter.
  *)
 
-let rec do_projection_effects 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 = Evd.define evk (mkVar id) evd 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 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
@@ -1110,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 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
 
@@ -1122,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
@@ -1133,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
@@ -1200,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
@@ -1225,35 +1268,22 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   else
     raise (CannotProject (evd,ev1'))
 
-let check_evar_instance evd evk1 body conv_algo =
-  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 *)
-  (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
-  let ty =
-    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 evenv evd Reduction.CUMUL ty evi.evar_concl with
-  | Success evd -> evd
-  | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl))
-
 let update_evar_info ev1 ev2 evd =
   (* We update the source of obligation evars during evar-evar unifications. *)
   let loc, evs1 = evar_source ev1 evd in
   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
 
@@ -1264,22 +1294,33 @@ let preferred_orientation evd evk1 evk2 =
   else if is_obligation_evar evd evk2 then false
   else true
 
-let solve_evar_evar_aux force 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_ev1 = Evar.Set.mem evk1 flags.frozen_evars 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 if not frozen_ev1 then
+        solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
+      else raise (CannotProject (evd,ev2))
     with CannotProject (evd,ev2) ->
-    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
-    with CannotProject (evd,ev1) ->
-    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
+      try if not frozen_ev2 then
+          solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
+        else raise (CannotProject (evd,ev1))
+      with CannotProject (evd,ev1) ->
+        add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
-    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
+    try if not frozen_ev2 then
+        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 if not frozen_ev1 then
+        solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
+      else raise (CannotProject (evd,ev2))
     with CannotProject (evd,ev2) ->
-    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
+      add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
-let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+(** Precondition: evk1 is not frozen *)
+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
@@ -1314,25 +1355,19 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
           downcast evk2 t2 (downcast evk1 t1 evd)
     with Reduction.NotArity -> 
       evd in
-  solve_evar_evar_aux force f g env evd pbty ev1 ev2
-
-type conv_fun =
-  env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result
-
-type conv_fun_bool =
-  env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool
+  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) 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
   | Some cstr ->
-    try ignore (Evd.add_universe_constraints !evdref cstr); true
+    try evdref := Evd.add_universe_constraints !evdref cstr; true
     with UniversesDiffer -> false
   in
   if Array.equal eq_constr argsv1 argsv2 then !evdref else
@@ -1340,19 +1375,26 @@ let solve_refl ?(can_drop=false) 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 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
+  let frozen = Evar.Set.mem evk flags.frozen_evars in
+  if Evar.equal (fst ev1) evk && (frozen || can_drop) then
+    (* No refinement needed *) 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 ev2 = (fst ev1,argsv2) in
-  (* Leave a unification problem *)
-  add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+  if frozen then
+    (* We cannot prune a frozen evar *)
+    add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd
+  else
+    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'
 
 (* If the evar can be instantiated by a finite set of candidates known
    in advance, we check which of them apply *)
@@ -1360,14 +1402,14 @@ let solve_refl ?(can_drop=false) 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] ->
@@ -1375,7 +1417,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
@@ -1399,6 +1441,13 @@ let occur_evar_upto_types sigma n c =
   in
   try occur_rec c; false with Occur -> true
 
+let instantiate_evar unify flags evd evk body =
+  (* 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'
+
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
@@ -1428,7 +1477,8 @@ exception NotEnoughInformationEvarEvar of EConstr.constr
 exception OccurCheckIn of evar_map * EConstr.constr
 exception MetaOccurInBodyInternal
 
-let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
+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
   let progress = ref false in
@@ -1447,7 +1497,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 (of_alias t)) in
-      let evd = do_projection_effects (evar_define 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
@@ -1460,7 +1510,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 ~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
@@ -1484,13 +1534,15 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | LocalAssum _ -> project_variable (RelAlias (i-k))
         | LocalDef (_,b,_) ->
           try project_variable (RelAlias (i-k))
-          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i (EConstr.of_constr b)))
+          with NotInvertibleUsingOurAlgorithm _ when imitate_defs ->
+            imitate envk (lift i (EConstr.of_constr b)))
     | Var id ->
         (match Environ.lookup_named id env' with
         | LocalAssum _ -> project_variable (VarAlias id)
         | LocalDef (_,b,_) ->
           try project_variable (VarAlias id)
-          with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b))
+          with NotInvertibleUsingOurAlgorithm _ when imitate_defs ->
+            imitate envk (EConstr.of_constr b))
     | LetIn (na,b,u,c) ->
         imitate envk (subst1 b c)
     | Evar (evk',args' as ev') ->
@@ -1499,7 +1551,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         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
@@ -1510,15 +1562,15 @@ 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' evd t in
           let (evd,evar'',ev'') =
-             materialize_evar (evar_define 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'') ->
@@ -1555,7 +1607,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 ~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 ->
@@ -1585,7 +1637,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     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)
 
@@ -1594,46 +1646,30 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
  * [define] tries to find an instance lhs such that
  * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in
  * context "hyps" and not referring to itself.
+ * ev is assumed not to be frozen.
  *)
 
-and evar_define conv_algo ?(choose=false) 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
-          (test_success conv_algo) env evd pbty evk argsv argsv2
+          (test_success unify) flags env evd pbty evk argsv argsv2
       else
         solve_evar_evar ~force:choose
-          (evar_define conv_algo) conv_algo env evd pbty ev ev2
+          (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 conv_algo choose 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
-(* Cannot strictly type instantiations since the unification algorithm
- * does not unify applications from left to right.
- * e.g problem f x == g y yields x==y and f==g (in that order)
- * Another problem is that type variables are evars of type Type
-   let _ =
-      try
-        let env = evar_filtered_env evi in
-        let ty = evi.evar_concl in
-        Typing.check env evd' body ty
-      with e ->
-        msg_info
-          (str "Ill-typed evar instantiation: " ++ fnl() ++
-           pr_evar_map evd' ++ fnl() ++
-           str "----> " ++ int ev ++ str " := " ++
-           print_constr body);
-        raise e in*)
-    let evd' = check_evar_instance evd' evk body conv_algo in
-    Evd.define evk body evd'
+    instantiate_evar unify flags evd' evk body
   with
     | NotEnoughInformationToProgress sols ->
         postpone_non_unique_projection env evd pbty ev sols rhs
@@ -1648,8 +1684,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         let c = whd_all env evd rhs in
         match EConstr.kind evd c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
-	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
-              env evd pbty evk argsv argsv2
+            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))
 
@@ -1683,13 +1719,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 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)
@@ -1702,11 +1738,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 conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
+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 conv_algo ~choose 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 4665ed29a2..ebf8230bbd 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,6 +16,25 @@ type alias
 
 val of_alias : alias -> EConstr.t
 
+type unify_flags = {
+  modulo_betaiota : bool;
+  (* Enable beta-iota reductions during unification *)
+  open_ts : TransparentState.t;
+  (* Enable delta reduction according to open_ts for open terms *)
+  closed_ts : TransparentState.t;
+  (* Enable delta reduction according to closed_ts for closed terms (when calling conversion) *)
+  subterm_ts : TransparentState.t;
+  (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
+     unifications. *)
+  frozen_evars : Evar.Set.t;
+  (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *)
+  allow_K_at_toplevel : bool;
+  (* During higher-order unifications, allow to produce K-redexes: i.e. to produce
+     an abstraction for an unused argument *)
+  with_cs : bool
+  (* Enable canonical structure resolution during unification *)
+}
+
 type unification_result =
   | Success of evar_map
   | UnifFailure of evar_map * Pretype_errors.unification_error
@@ -26,19 +45,49 @@ 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
 
+(** 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. *)
+
+type unification_kind =
+  | TypeUnification
+  | TermUnification
+
+(** 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 = unify_flags -> unification_kind ->
+  env -> evar_map -> conv_pb -> constr -> constr -> bool
+
+(** [instantiate_evar unify flags env sigma ev c] defines the evar [ev] with [c],
+    checking that the type of [c] is unifiable with [ev]'s declared type first.
+
+    Preconditions:
+    - [ev] does not occur in [c].
+    - [c] does not contain any Meta(_)
+ *)
+
+val instantiate_evar : unifier -> unify_flags -> evar_map ->
+  Evar.t -> constr -> evar_map
+
 (** [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] *)
 
-type conv_fun =
-  env ->  evar_map -> conv_pb -> constr -> constr -> unification_result
-
-type conv_fun_bool =
-  env ->  evar_map -> conv_pb -> constr -> constr -> bool
+val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool ->
+  env -> evar_map -> bool option -> existential -> constr -> evar_map
 
-val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
-  bool option -> existential -> constr -> evar_map
 
 val refresh_universes :
   ?status:Evd.rigid ->
@@ -49,18 +98,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 -> conv_fun_bool -> 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 ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
-  conv_fun ->
+  unifier -> unify_flags ->
   env ->  evar_map -> bool option -> existential -> existential -> evar_map
 
-val solve_simple_eqn : conv_fun -> ?choose: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 : conv_fun -> 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
@@ -75,8 +124,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 -> conv_fun -> 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/find_subterm.ml b/pretyping/find_subterm.ml
index b16087031b..d150f8e1cb 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -125,7 +125,7 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
          end;
          add_subst t subst; incr pos;
          (* Check nested matching subterms *)
-         if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then
+         if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then
            begin nested := true; ignore (subst_below k t); nested := false end;
          (* Do the effective substitution *)
          Vars.lift k (bywhat ()))
diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 37dd120c1a..087a6b9174 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -20,6 +20,7 @@ type 'a or_var =
 
 type 'a occurrences_gen =
   | AllOccurrences
+  | AtLeastOneOccurrence
   | AllOccurrencesBut of 'a list (** non-empty *)
   | NoOccurrences
   | OnlyOccurrences of 'a list (** non-empty *)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 6b6a3f8a9f..aaa4ce684d 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -19,15 +19,17 @@ let occurrences_map f = function
   | AllOccurrencesBut l ->
     let l' = f l in
     if l' = [] then AllOccurrences else AllOccurrencesBut l'
-  | (NoOccurrences|AllOccurrences) as o -> o
+  | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o
 
 let convert_occs = function
+  | AtLeastOneOccurrence -> (false,[])
   | AllOccurrences -> (false,[])
   | AllOccurrencesBut l -> (false,l)
   | NoOccurrences -> (true,[])
   | OnlyOccurrences l -> (true,l)
 
 let is_selected occ = function
+  | AtLeastOneOccurrence -> true
   | AllOccurrences -> true
   | AllOccurrencesBut l -> not (Int.List.mem occ l)
   | OnlyOccurrences l -> Int.List.mem occ l
@@ -46,6 +48,11 @@ let is_nowhere = function
 | { onhyps=Some[]; concl_occs=NoOccurrences } -> true
 | _ -> false
 
+let is_all_occurrences = function
+  | AtLeastOneOccurrence
+  | AllOccurrences -> true
+  | _ -> false
+
 (** Clause conversion functions, parametrized by a hyp enumeration function *)
 
 (** From [clause] to [simple_clause] *)
@@ -61,12 +68,12 @@ let simple_clause_of enum_hyps cl =
 	List.map Option.make (enum_hyps ())
     | Some l ->
 	List.map (fun ((occs,id),w) ->
-	  if occs <> AllOccurrences then error_occurrences ();
+          if not (is_all_occurrences occs) then error_occurrences ();
 	  if w = InHypValueOnly then error_body_selection ();
 	  Some id) l in
   if cl.concl_occs = NoOccurrences then hyps
   else
-    if cl.concl_occs <> AllOccurrences then error_occurrences ()
+    if not (is_all_occurrences cl.concl_occs) then error_occurrences ()
     else None :: hyps
 
 (** From [clause] to [concrete_clause] *)
@@ -111,7 +118,7 @@ let clause_with_generic_occurrences cls =
      List.for_all
        (function ((AllOccurrences,_),_) -> true | _ -> false) hyps in
   let concl = match cls.concl_occs with
-  | AllOccurrences | NoOccurrences -> true
+  | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
   | _ -> false in
   hyps && concl
 
@@ -122,6 +129,6 @@ let clause_with_generic_context_selection cls =
      List.for_all
        (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in
   let concl = match cls.concl_occs with
-  | AllOccurrences | NoOccurrences -> true
+  | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
   | _ -> false in
   hyps && concl
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index a07c018c32..ac15fe1018 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -21,6 +21,8 @@ val convert_occs : occurrences -> bool * int list
 
 val is_selected : int -> occurrences -> bool
 
+val is_all_occurrences : 'a occurrences_gen -> bool
+
 (** Usual clauses *)
 
 val allHypsAndConcl : 'a clause_expr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a92b245b91..9612932439 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -266,7 +266,7 @@ let apply_inference_hook hook env sigma frozen = match frozen with
 let apply_heuristics env sigma fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
   try solve_unif_constraints_with_heuristics
-        ~ts:(Typeclasses.classes_transparent_state ()) env sigma
+        ~flags:(default_flags_of (Typeclasses.classes_transparent_state ())) env sigma
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     if fail_evar then iraise e else sigma
@@ -562,9 +562,9 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
 	  | GFix (vn,i) -> i
 	  | GCoFix i -> i
         in
-        begin match conv !!env sigma ftys.(fixi) t with
-          | None -> sigma
-          | Some sigma -> sigma
+        begin match Evarconv.unify_delay !!env sigma ftys.(fixi) t with
+          | exception Evarconv.UnableToUnify _ -> sigma
+          | sigma -> sigma
         end
       | None -> sigma
     in
@@ -670,11 +670,11 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
             match candargs with
             | [] -> sigma, [], j_val hj
             | arg :: args ->
-              begin match conv !!env sigma (j_val hj) arg with
-                | Some sigma ->
-                  sigma, args, nf_evar sigma (j_val hj)
-                | None ->
+              begin match Evarconv.unify_delay !!env sigma (j_val hj) arg with
+                | exception Evarconv.UnableToUnify _ ->
                   sigma, [], j_val hj
+                | sigma ->
+                  sigma, args, nf_evar sigma (j_val hj)
               end
           in
             let sigma, ujval = adjust_evar_source sigma na ujval in
@@ -1060,9 +1060,9 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
 	match valcon with
         | None -> sigma, tj
 	| Some v ->
-          begin match cumul !!env sigma v tj.utj_val with
-            | Some sigma -> sigma, tj
-            | None ->
+          begin match Evarconv.unify_leq_delay !!env sigma v tj.utj_val with
+            | sigma -> sigma, tj
+            | exception Evarconv.UnableToUnify _ ->
 	      error_unexpected_type
                 ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v
           end
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2308a541fb..5db571433a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1105,6 +1105,7 @@ let unfoldoccs env sigma (occs,name) c =
     | AllOccurrences -> unfold env sigma name c
     | OnlyOccurrences l -> unfo true l
     | AllOccurrencesBut l -> unfo false l
+    | AtLeastOneOccurrence -> unfo false []
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2e50e1ab3f..ea6e52e1f8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -71,10 +71,10 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
          | _ ->
              error_cant_apply_not_functional env sigma funj argjv
        in
-       begin match Evarconv.cumul env sigma hj.uj_type c1 with
-         | Some sigma ->
+       begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with
+         | sigma ->
            apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
-         | None ->
+         | exception Evarconv.UnableToUnify _ ->
            error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
        end
   in
@@ -96,10 +96,10 @@ let judge_of_apply env sigma funj argjv =
          | _ ->
             error_cant_apply_not_functional env sigma funj argjv
        in
-       begin match Evarconv.cumul env sigma hj.uj_type c1 with
-         | Some sigma ->
+       begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with
+         | sigma ->
            apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
-         | None ->
+         | exception Evarconv.UnableToUnify _ ->
            error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
        end
   in
@@ -109,9 +109,9 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
     error_number_branches env sigma cj (Array.length explft);
   Array.fold_left2_i (fun i sigma lfj explft ->
-      match Evarconv.cumul env sigma lfj.uj_type explft with
-      | Some sigma -> sigma
-      | None ->
+      match Evarconv.unify_leq_delay env sigma lfj.uj_type explft with
+      | sigma -> sigma
+      | exception Evarconv.UnableToUnify _ ->
         error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft)
     sigma lfj explft
 
@@ -127,9 +127,9 @@ let is_correct_arity env sigma c pj ind specif params =
     let pt' = whd_all env sigma pt in
     match EConstr.kind sigma pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-      begin match Evarconv.cumul env sigma a1 a1' with
-        | None -> error ()
-        | Some sigma ->
+      begin match Evarconv.unify_leq_delay env sigma a1 a1' with
+        | exception Evarconv.UnableToUnify _ -> error ()
+        | sigma ->
           srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar'
       end
     | Sort s, [] ->
@@ -187,9 +187,9 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
   let lt = Array.length vdefj in
   assert (Int.equal (Array.length lar) lt);
   Array.fold_left2_i (fun i sigma defj ar ->
-      match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with
-      | Some sigma -> sigma
-      | None ->
+      match Evarconv.unify_leq_delay env sigma defj.uj_type (lift lt ar) with
+      | sigma -> sigma
+      | exception Evarconv.UnableToUnify _ ->
         error_ill_typed_rec_body ?loc env sigma
           i lna vdefj lar)
     sigma vdefj lar
@@ -211,10 +211,10 @@ let check_allowed_sort env sigma ind c p =
 
 let judge_of_cast env sigma cj k tj =
   let expected_type = tj.utj_val in
-  match Evarconv.cumul env sigma cj.uj_type expected_type with
-  | None ->
+  match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with
+  | exception Evarconv.UnableToUnify _ ->
     error_actual_type_core env sigma cj expected_type;
-  | Some sigma ->
+  | sigma ->
     sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
              uj_type = expected_type }
 
@@ -427,10 +427,10 @@ and execute_array env = Array.fold_left_map (execute env)
 
 let check env sigma c t =
   let sigma, j = execute env sigma c in
-  match Evarconv.cumul env sigma j.uj_type t with
-  | None ->
+  match Evarconv.unify_leq_delay env sigma j.uj_type t with
+  | exception Evarconv.UnableToUnify _ ->
     error_actual_type_core env sigma j t
-  | Some sigma -> sigma
+  | sigma -> sigma
 
 (* Type of a constr *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ac0b58b92b..3de8c381d0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -141,7 +141,15 @@ let abstract_list_all env evd typ c l =
   evd,(p,typp)
 
 let set_occurrences_of_last_arg args =
-  Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
+  Evarconv.AtOccurrences AllOccurrences ::
+    List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args)
+
+let occurrence_test _ _ _ env sigma _ c1 c2 =
+  match EConstr.eq_constr_universes env sigma c1 c2 with
+  | None -> false, sigma
+  | Some cstr ->
+     try true, Evd.add_universe_constraints sigma cstr
+     with UniversesDiffer -> false, sigma
 
 let abstract_list_all_with_dependencies env evd typ c l =
   let (evd, ev) = new_evar env evd typ in
@@ -149,8 +157,9 @@ let abstract_list_all_with_dependencies env evd typ c l =
   let n = List.length l in
   let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
   let evd,b =
-    Evarconv.second_order_matching TransparentState.empty
-      env evd ev' argoccs c in
+    Evarconv.second_order_matching
+      (Evarconv.default_flags_of TransparentState.empty)
+      env evd ev' (occurrence_test, argoccs) c in
   if b then
     let p = nf_evar evd ev in
       evd, p
@@ -1315,8 +1324,8 @@ let order_metas metas =
 
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
-let solve_simple_evar_eqn ts env evd ev rhs =
-  match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
+let solve_simple_evar_eqn flags env evd ev rhs =
+  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
@@ -1326,6 +1335,7 @@ let solve_simple_evar_eqn ts env evd ev rhs =
    is true, unification of types of metas is required *)
 
 let w_merge env with_types flags (evd,metas,evars : subst0) =
+  let eflags = Evarconv.default_flags_of flags.modulo_delta_types in
   let rec w_merge_rec evd metas evars eqns =
 
     (* Process evars *)
@@ -1350,14 +1360,14 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
 	      else
 		let evd' = 
 		  let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
-		    try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs''
+                  try solve_simple_evar_eqn eflags curenv evd' ev rhs''
 		    with Retyping.RetypeError _ ->
 		      error_cannot_unify curenv evd' (mkEvar ev,rhs'')
 		in w_merge_rec evd' metas evars' eqns
           | _ ->
 	      let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
 	      let evd' = 
-		try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs''
+                try solve_simple_evar_eqn eflags curenv evd' ev rhs''
 		with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'')
 	      in
 		w_merge_rec evd' metas evars' eqns
@@ -1649,7 +1659,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     match occurrences_of_hyp hyp occs with
     | NoOccurrences, InHyp ->
         (push_named_context_val d sign,depdecls)
-    | AllOccurrences, InHyp as occ ->
+    | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
         let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
         if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 1b2756f49f..0f97a942ed 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -37,8 +37,8 @@ let define_and_solve_constraints evk c env evd =
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-        | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2
-	| UnifFailure _ as x -> x) (Success evd)
+        | Success evd -> Evarconv.evar_conv_x (Evarconv.default_flags_of TransparentState.full) env evd pbty t1 t2
+        | UnifFailure _ as x -> x) (Success evd)
       pbs
   with
     | Success evd -> evd
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7245d4a004..e5688fe730 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -58,10 +58,11 @@ module V82 = struct
        created. *)
     let prev_future_goals = Evd.save_future_goals evars in
     let evi = { Evd.evar_hyps = hyps;
-		Evd.evar_concl = concl;
-		Evd.evar_filter = Evd.Filter.identity;
-		Evd.evar_body = Evd.Evar_empty;
-		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
+                Evd.evar_concl = concl;
+                Evd.evar_filter = Evd.Filter.identity;
+                Evd.evar_abstract_arguments = Evd.Abstraction.identity;
+                Evd.evar_body = Evd.Evar_empty;
+                Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
                 Evd.evar_candidates = None }
     in
     let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index f824552705..3b8232d20a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -145,7 +145,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
   let try_do_hyps treat_id l =
     autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas
   in
-  if cl.concl_occs != AllOccurrences &&
+  if not (Locusops.is_all_occurrences cl.concl_occs) &&
      cl.concl_occs != NoOccurrences
   then
     Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e505bb3a42..a3620f4081 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -230,8 +230,9 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
       let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
       let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
       let sigma' =
-        Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta
-                                cl.cl_concl concl sigma'
+        Evarconv.(unify_leq_delay
+                    ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
+                              env sigma' cl.cl_concl concl)
       in (sigma', term) end
 
 let unify_resolve_refine poly flags gl clenv =
@@ -1111,7 +1112,7 @@ let initial_select_evars filter =
 let resolve_typeclass_evars debug depth unique env evd filter split fail =
   let evd =
     try Evarconv.solve_unif_constraints_with_heuristics
-      ~ts:(Typeclasses.classes_transparent_state ()) env evd
+      ~flags:(Evarconv.default_flags_of (Typeclasses.classes_transparent_state ())) env evd
     with e when CErrors.noncritical e -> evd
   in
     resolve_all_evars debug depth unique env
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 769e702da1..4a1bb37fa4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -437,7 +437,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 
 let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     ((c,l) : constr with_bindings) with_evars =
-  if occs != AllOccurrences then (
+  if not (Locusops.is_all_occurrences occs) then (
     rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
   else
     Proofview.Goal.enter begin fun gl ->
@@ -595,15 +595,16 @@ let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
   else check_required_library ["Coq";"Setoids";"Setoid"]
 
-let check_setoid cl = 
+let check_setoid cl =
+  let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in
   Option.fold_left
-    ( List.fold_left 
+    (List.fold_left
 	(fun b ((occ,_),_) -> 
-	  b||(Locusops.occurrences_map (fun x -> x) occ <> AllOccurrences)
+          b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ)))
 	)
     )
-    ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) &&
-	(Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences))
+    (not (Locusops.is_all_occurrences concloccs) &&
+     (concloccs <> NoOccurrences))
     cl.onhyps
 
 let replace_core clause l2r eq =
@@ -635,7 +636,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
-      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
+      try Some (Evarconv.unify_delay (Proofview.Goal.env gl) (Tacmach.New.project gl) t1 t2)
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -1193,9 +1194,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       (* is the default value typable with the expected type *)
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
-        let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in
-        let sigma =
-          Evarconv.solve_unif_constraints_with_heuristics env sigma in
+        let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in
+        let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
         sigma, dflt
       with Evarconv.UnableToUnify _ ->
 	user_err Pp.(str "Cannot solve a unification problem.")
@@ -1210,11 +1210,11 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       match evopt with
 	| Some w ->
           let w_type = unsafe_type_of env sigma w in
-          begin match Evarconv.cumul env sigma w_type a with
-            | Some sigma ->
+          begin match Evarconv.unify_leq_delay env sigma w_type a with
+            | sigma ->
               let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
               sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
-            | None ->
+            | exception Evarconv.UnableToUnify _ ->
               user_err Pp.(str "Cannot solve a unification problem.")
           end
 	| None ->
@@ -1724,7 +1724,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   tclTHENLIST
     ((if need_rewrite then
       [revert (List.map snd dephyps);
-       general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
+       general_rewrite dir AtLeastOneOccurrence true dep_proof_ok (mkVar hyp);
        (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)]
       else
        [Proofview.tclUNIT ()]) @
diff --git a/tactics/ppred.ml b/tactics/ppred.ml
index dd1bcd4699..d832dc279c 100644
--- a/tactics/ppred.ml
+++ b/tactics/ppred.ml
@@ -6,6 +6,7 @@ open Pputils
 
 let pr_with_occurrences pr keyword (occs,c) =
   match occs with
+    | AtLeastOneOccurrence -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" +")
     | AllOccurrences ->
       pr c
     | NoOccurrences ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index db59f7cfc2..415225454a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3840,9 +3840,9 @@ let specialize_eqs id =
   let evars = ref (Proofview.Goal.sigma gl) in
   let unif env evars c1 c2 =
     compare_upto_variables !evars c1 c2 &&
-    (match Evarconv.conv env !evars c1 c2 with
-     | Some sigma -> evars := sigma; true
-     | None -> false)
+    (match Evarconv.unify_delay env !evars c1 c2 with
+     | sigma -> evars := sigma; true
+     | exception Evarconv.UnableToUnify _ -> false)
   in
   let rec aux in_eqs ctx acc ty =
     match EConstr.kind !evars ty with
@@ -4398,7 +4398,9 @@ let check_expected_type env sigma (elimc,bl) elimt =
   let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
   let sigma = solve_evar_clause env sigma true cl bl in
   let (_,u,_) = destProd sigma cl.cl_concl in
-  fun t -> Option.has_some (Evarconv.cumul env sigma t u)
+  fun t -> match Evarconv.unify_leq_delay env sigma t u with
+    | _sigma -> true
+    | exception Evarconv.UnableToUnify _ -> false
 
 let check_enough_applied env sigma elim =
   (* A heuristic to decide whether the induction arg is enough applied *)