A step towards better differentiating when w_unify is used for subterm

selection (rewrite, destruct/induction, set or apply on scheme), for
unification (apply on not a scheme, auto), the latter being separated
into primary unification and unification for merging instances.

No change of semantics from within Coq, if I did not mistake (but a
function like secondOrderAbstraction does not set flags by itself
anymore).

11 files changed, 275 insertions, 154 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d5dfd7bf00..9737b9feb1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -211,7 +211,7 @@ let _ =
       optread  = (fun () -> !global_evars_pattern_unification_flag);
       optwrite = (:=) global_evars_pattern_unification_flag }
 
-type unify_flags = {
+type core_unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
     (* What this flag controls was activated with all constants transparent, *)
     (* even for auto, since Coq V5.10 *)
@@ -226,21 +226,10 @@ type unify_flags = {
 
   modulo_delta_types : Names.transparent_state;
 
-  modulo_delta_in_merge : Names.transparent_state option;
-    (* This controls whether unfoldability is different when trying to unify *)
-    (* several instances of the same metavariable *)
-    (* Typical situation is when we give a pattern to be matched *)
-    (* syntactically against a subterm but we want the metas of the *)
-    (* pattern to be modulo convertibility *)
-
   check_applied_meta_types : bool;
     (* This controls whether meta's applied to arguments have their *)
     (* type unified with the type of their instance *)
 
-  resolve_evars : bool;
-    (* This says if type classes instances resolution must be used to infer *)
-    (* the remaining evars *)
-
   use_pattern_unification : bool;
     (* This says if type classes instances resolution must be used to infer *)
     (* the remaining evars *)
@@ -263,44 +252,67 @@ type unify_flags = {
 
   modulo_eta : bool;
     (* Support eta in the reduction *)
+}
 
-  allow_K_in_toplevel_higher_order_unification : bool
-    (* This is used only in second/higher order unification when looking for *)
-    (* subterms (rewrite and elim) *)
+type unify_flags = {
+  core_unify_flags : core_unify_flags;
+    (* Governs unification of problems of the form "t(?x) = u(?x)" in apply *)
+
+  merge_unify_flags : core_unify_flags;
+    (* These are the flags to be used when trying to unify *)
+    (* several instances of the same metavariable *)
+    (* Typical situation is when we give a pattern to be matched *)
+    (* syntactically against a subterm but we want the metas of the *)
+    (* pattern to be modulo convertibility *)
+
+  subterm_unify_flags : core_unify_flags;
+    (* Governs unification of problems of the form "?X a1..an = u" in apply, *)
+    (* hence in rewrite and elim *)
+
+  allow_K_in_toplevel_higher_order_unification : bool;
+    (* Tells in second-order abstraction over subterms which have not *)
+    (* been found in term are allowed (used for rewrite, elim, or *)
+    (* apply with a lemma whose type has the form "?X a1 ... an") *)
+
+  resolve_evars : bool
+    (* This says if type classes instances resolution must be used to infer *)
+    (* the remaining evars *)
 }
 
 (* Default flag for unifying a type against a type (e.g. apply) *)
 (* We set all conversion flags (no flag should be modified anymore) *)
-let default_unify_flags () = 
-  let ts = Names.full_transparent_state in
-  { modulo_conv_on_closed_terms = Some ts;
+let default_core_unify_flags () =
+  let ts = Names.full_transparent_state in {
+  modulo_conv_on_closed_terms = Some ts;
   use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = ts;
   modulo_delta_types = ts;
-  modulo_delta_in_merge = None;
   check_applied_meta_types = true;
-  resolve_evars = false;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
   frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;
   modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = false
-      (* in fact useless when not used in w_unify_to_subterm_list *)
+ }
+
+(* Default flag for first-order or second-order unification of a type *)
+(* against another type (e.g. apply)                                  *)
+(* We set all conversion flags (no flag should be modified anymore)   *)
+let default_unify_flags () =
+  let flags = default_core_unify_flags () in {
+  core_unify_flags = flags;
+  merge_unify_flags = flags;
+  subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
+  allow_K_in_toplevel_higher_order_unification = false; (* Why not? *)
+  resolve_evars = false
 }
 
-let set_merge_flags flags =
-  match flags.modulo_delta_in_merge with
-  | None -> flags
-  | Some ts ->
-    { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts }
-
 (* Default flag for the "simple apply" version of unification of a *)
 (* type against a type (e.g. apply) *)
-(* We set only the flags available at the time the new "apply" extends *)
+(* We set only the flags available at the time the new "apply" extended *)
 (* out of "simple apply" *)
-let default_no_delta_unify_flags () = { (default_unify_flags ()) with
+let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with
   modulo_delta = empty_transparent_state;
   check_applied_meta_types = false;
   use_pattern_unification = false;
@@ -308,21 +320,47 @@ let default_no_delta_unify_flags () = { (default_unify_flags ()) with
   modulo_betaiota = false;
 }
 
+let default_no_delta_unify_flags () =
+  let flags = default_no_delta_core_unify_flags () in {
+  core_unify_flags = flags;
+  merge_unify_flags = flags;
+  subterm_unify_flags = flags;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
+}
+
 (* Default flags for looking for subterms in elimination tactics *)
 (* Not used in practice at the current date, to the exception of *)
 (* allow_K) because only closed terms are involved in *)
 (* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
 (* call w_unify for induction/destruct/case/elim  (13/6/2011) *)
-let elim_flags () = { (default_unify_flags ()) with
-  restrict_conv_on_strict_subterms = false; (* ? *)
+let elim_core_flags () = { (default_core_unify_flags ()) with
   modulo_betaiota = false;
-  allow_K_in_toplevel_higher_order_unification = true
 }
 
-let elim_no_delta_flags () = { (elim_flags ()) with
+let elim_flags () =
+  let flags = elim_core_flags () in {
+  core_unify_flags = flags;
+  merge_unify_flags = flags;
+  subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
+  allow_K_in_toplevel_higher_order_unification = true;
+  resolve_evars = false
+}
+
+let elim_no_delta_core_flags () = { (elim_core_flags ()) with
   modulo_delta = empty_transparent_state;
   check_applied_meta_types = false;
   use_pattern_unification = false;
+  modulo_betaiota = false;
+}
+
+let elim_no_delta_flags () =
+  let flags = elim_no_delta_core_flags () in {
+  core_unify_flags = flags;
+  merge_unify_flags = flags;
+  subterm_unify_flags = flags;
+  allow_K_in_toplevel_higher_order_unification = true;
+  resolve_evars = false
 }
 
 let use_evars_pattern_unification flags =
@@ -1034,7 +1072,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	if Evd.is_defined evd evk then
 	  let v = Evd.existential_value evd ev in
 	  let (evd,metas',evars'') =
-	    unify_0 curenv evd CONV (set_merge_flags flags) rhs v in
+	    unify_0 curenv evd CONV flags rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
 	  (* This can make rhs' ill-typed if metas are *)
@@ -1114,7 +1152,7 @@ let w_merge env with_types flags (evd,metas,evars) =
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
-      unify_0 sp_env evd' CUMUL (set_merge_flags flags)
+      unify_0 sp_env evd' CUMUL flags
         (get_type_of sp_env evd' c) ev.evar_concl in
     let evd''' = w_merge_rec evd'' mc ec [] in
     if evd' == evd'''
@@ -1137,7 +1175,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 
 let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
   let metas,evd = retract_coercible_metas evd in
-  w_merge env true flags (evd,metas,[])
+  w_merge env true flags.merge_unify_flags (evd,metas,[])
 
 (* [w_unify env evd M N]
    performs a unification of M and N, generating a bunch of
@@ -1165,32 +1203,33 @@ let check_types env flags (sigma,_,_ as subst) m n =
       (get_type_of env sigma n)
   else subst
 
-let try_resolve_typeclasses env evd flags m n =
-  if flags.resolve_evars then
+let try_resolve_typeclasses env evd flag m n =
+  if flag then
     Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false
       ~fail:true env evd
   else evd
 
 let w_unify_core_0 env evd with_types cv_pb flags m n =
   let (mc1,evd') = retract_coercible_metas evd in
-  let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in
+  let (sigma,ms,es) = check_types env flags.core_unify_flags (evd,mc1,[]) m n in
   let subst2 =
-     unify_0_with_initial_metas (evd',ms,es) false env cv_pb flags m n
+     unify_0_with_initial_metas (evd',ms,es) false env cv_pb
+       flags.core_unify_flags m n
   in
-  let evd = w_merge env with_types flags subst2 in
-  try_resolve_typeclasses env evd flags m n
+  let evd = w_merge env with_types flags.merge_unify_flags subst2 in
+  try_resolve_typeclasses env evd flags.resolve_evars m n
 
 let w_typed_unify env evd = w_unify_core_0 env evd true
 
 let w_typed_unify_array env evd flags f1 l1 f2 l2 =
-  let flags' = { flags with resolve_evars = false } in
   let f1,l1,f2,l2 = adjust_app_array_size f1 l1 f2 l2 in
   let (mc1,evd') = retract_coercible_metas evd in
-  let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags' m n in
+  let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags.core_unify_flags  m n in
   let subst = fold_subst (evd', [], []) f1 f2 in
   let subst = Array.fold_left2 fold_subst subst l1 l2 in
-  let evd = w_merge env true flags subst in
-  try_resolve_typeclasses env evd flags (mkApp(f1,l1)) (mkApp(f2,l2))
+  let evd = w_merge env true flags.merge_unify_flags subst in
+  try_resolve_typeclasses env evd flags.resolve_evars
+    (mkApp(f1,l1)) (mkApp(f2,l2))
 
 (* takes a substitution s, an open term op and a closed term cl
    try to find a subterm of cl which matches op, if op is just a Meta
@@ -1243,14 +1282,13 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sig
   let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
   in Evd.evar_universe_context sigma, nf_evar sigma c
 
-let default_matching_flags sigma = {
+let default_matching_core_flags sigma =
+  let ts = Names.full_transparent_state in {
   modulo_conv_on_closed_terms = Some empty_transparent_state;
   use_metas_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
-  modulo_delta_in_merge = Some full_transparent_state;
+  modulo_delta_types = ts;
   check_applied_meta_types = true;
-  resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = false;
   frozen_evars =
@@ -1259,7 +1297,26 @@ let default_matching_flags sigma = {
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
   modulo_eta = false;
-  allow_K_in_toplevel_higher_order_unification = false
+}
+
+let default_matching_merge_flags sigma =
+  let ts = Names.full_transparent_state in
+  let flags = default_matching_core_flags sigma in {
+  flags with
+    modulo_conv_on_closed_terms = Some ts;
+    modulo_delta = ts;
+    modulo_betaiota = true;
+    modulo_eta = true;
+    use_pattern_unification = true;
+}
+
+let default_matching_flags sigma =
+  let flags = default_matching_core_flags sigma in {
+  core_unify_flags = flags;
+  merge_unify_flags = default_matching_merge_flags sigma;
+  subterm_unify_flags = flags; (* does not matter *)
+  resolve_evars = false;
+  allow_K_in_toplevel_higher_order_unification = false;
 }
 
 (* This supports search of occurrences of term from a pattern *)
@@ -1539,15 +1596,16 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
 
 let secondOrderAbstraction env evd flags typ (p, oplist) =
   (* Remove delta when looking for a subterm *)
-  let flags = { flags with modulo_delta = empty_transparent_state } in
+  let flags = { flags with core_unify_flags = flags.subterm_unify_flags } in
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
   let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
   let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in
-    if not b then
-      error_wrong_abstraction_type env evd'
-  	(Evd.meta_name evd p) pred typp predtyp;
-    w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[])
+  if not b then
+    error_wrong_abstraction_type env evd'
+      (Evd.meta_name evd p) pred typp predtyp;
+  w_merge env false flags.merge_unify_flags
+    (evd',[p,pred,(Conv,TypeProcessed)],[])
 
   (* let evd',metas,evars =  *)
   (*   try unify_0 env evd' CUMUL flags predtyp typp  *)
@@ -1560,7 +1618,8 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
   let typp = Typing.meta_type evd p in
   let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
-  w_merge env false flags (evd,[p,pred,(Conv,TypeProcessed)],[])
+  w_merge env false flags.merge_unify_flags
+    (evd,[p,pred,(Conv,TypeProcessed)],[])
 
 let secondOrderAbstractionAlgo dep =
   if dep then secondOrderDependentAbstraction else secondOrderAbstraction
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index de8eecc274..bedd6bf161 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -10,23 +10,31 @@ open Term
 open Environ
 open Evd
 
-type unify_flags = {
+type core_unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly_in_conv_on_closed_terms : bool;
   modulo_delta : Names.transparent_state;
   modulo_delta_types : Names.transparent_state;
-  modulo_delta_in_merge : Names.transparent_state option;
   check_applied_meta_types : bool;
-  resolve_evars : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
   frozen_evars : Evar.Set.t;
   restrict_conv_on_strict_subterms : bool;
   modulo_betaiota : bool;
   modulo_eta : bool;
-  allow_K_in_toplevel_higher_order_unification : bool
 }
 
+type unify_flags = {
+  core_unify_flags : core_unify_flags;
+  merge_unify_flags : core_unify_flags;
+  subterm_unify_flags : core_unify_flags;
+  allow_K_in_toplevel_higher_order_unification : bool;
+  resolve_evars : bool
+}
+
+val default_core_unify_flags : unit -> core_unify_flags
+val default_no_delta_core_unify_flags : unit -> core_unify_flags
+
 val default_unify_flags : unit -> unify_flags
 val default_no_delta_unify_flags : unit -> unify_flags
 
@@ -79,14 +87,14 @@ val abstract_list_all :
 
 (* For tracing *)
 
-val w_merge : env -> bool -> unify_flags -> evar_map *
+val w_merge : env -> bool -> core_unify_flags -> evar_map *
   (metavariable * constr * (instance_constraint * instance_typing_status)) list *
   (env * types pexistential * types) list -> evar_map
 
 val unify_0 :            Environ.env ->
            Evd.evar_map ->
            Evd.conv_pb ->
-           unify_flags ->
+           core_unify_flags ->
            Term.types ->
            Term.types ->
            Evd.evar_map * Evd.metabinding list *
@@ -98,7 +106,7 @@ val unify_0_with_initial_metas :
            bool ->
            Environ.env ->
            Evd.conv_pb ->
-           unify_flags ->
+           core_unify_flags ->
            Term.types ->
            Term.types ->
            Evd.evar_map * Evd.metabinding list *
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 33df4ca978..c6f0f2ee0d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -360,7 +360,7 @@ let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv =
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
-    clenv_unify ~flags:flags CUMUL
+    clenv_unify ~flags CUMUL
       (clenv_term clenv' nextclenv.templtyp)
       (clenv_meta_type clenv' mv)
       clenv' in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index d4826ce202..94731b0394 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -93,21 +93,26 @@ let res_pf ?(with_evars=false) ?(flags=dft ()) clenv =
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
-let fail_quick_unif_flags = {
+let fail_quick_core_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
-  modulo_delta_in_merge = None;
   check_applied_meta_types = false;
-  resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
   frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = false
+}
+
+let fail_quick_unif_flags = {
+  core_unify_flags = fail_quick_core_unif_flags;
+  merge_unify_flags = fail_quick_core_unif_flags;
+  subterm_unify_flags = fail_quick_core_unif_flags;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d269bf02d8..67484429f2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1113,23 +1113,35 @@ let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
 
 open Unification
 
-let auto_unif_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = false;
-  modulo_delta = empty_transparent_state;
+let auto_core_unif_flags_of st1 st2 useeager = {
+  modulo_conv_on_closed_terms = Some st1;
+  use_metas_eagerly_in_conv_on_closed_terms = useeager;
+  modulo_delta = st2;
   modulo_delta_types = full_transparent_state;
-  modulo_delta_in_merge = None;
   check_applied_meta_types = false;
-  resolve_evars = true;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
   frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false; (* Compat *)
   modulo_betaiota = false;
   modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = false
 }
 
+let auto_unif_flags_of st1 st2 useeager =
+  let flags = auto_core_unif_flags_of st1 st2 useeager in {
+  core_unify_flags = flags;
+  merge_unify_flags = flags;
+  subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = true
+}
+
+let auto_unif_flags =
+  auto_unif_flags_of full_transparent_state empty_transparent_state false
+
+let auto_flags_of_state st =
+  auto_unif_flags_of full_transparent_state st false
+
 (* Try unification with the precompiled clause, then use registered Apply *)
 
 let unify_resolve_nodelta poly (c,clenv) gl =
@@ -1370,9 +1382,14 @@ let tclTRY_dbg d tac =
 (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
   de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
 
+let auto_unif_flags =
+  auto_unif_flags_of full_transparent_state empty_transparent_state false
+
 let flags_of_state st =
-  {auto_unif_flags with
-    modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+  auto_unif_flags_of st st false
+
+let auto_flags_of_state st =
+  auto_unif_flags_of full_transparent_state st false
 
 let hintmap_of hdc concl =
   match hdc with
@@ -1418,7 +1435,6 @@ and my_find_search mod_delta =
   else my_find_search_nodelta
 
 and my_find_search_delta db_list local_db hdc concl =
-  let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in
   let f = hintmap_of hdc concl in
     if occur_existential concl then
       List.map_append
@@ -1427,7 +1443,7 @@ and my_find_search_delta db_list local_db hdc concl =
 	    let flags = flags_of_state (Hint_db.transparent_state db) in
 	      List.map (fun x -> (Some flags,x)) (f db)
 	  else
-	    let flags = {flags with modulo_delta = Hint_db.transparent_state db} in
+	    let flags = auto_flags_of_state (Hint_db.transparent_state db) in
 	      List.map (fun x -> (Some flags,x)) (f db))
 	(local_db::db_list)
     else
@@ -1444,7 +1460,7 @@ and my_find_search_delta db_list local_db hdc concl =
 		  if (Id.Pred.is_empty ids && Cpred.is_empty csts)
 		  then Hint_db.map_auto (hdc,concl) db
 		  else Hint_db.map_all hdc db
-	    in {flags with modulo_delta = st}, l
+	    in auto_flags_of_state st, l
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index b85f86ea48..3c916af733 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -201,7 +201,7 @@ val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
 
 val default_search_depth : int ref
 
-val auto_unif_flags : Unification.unify_flags
+val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve_nodelta : polymorphic -> (constr * clausenv) -> tactic
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c741610a37..e298c31cb1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -52,21 +52,26 @@ open Auto
 
 open Unification
 
-let auto_unif_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
+let auto_core_unif_flags st = {
+  modulo_conv_on_closed_terms = Some st;
   use_metas_eagerly_in_conv_on_closed_terms = true;
-  modulo_delta = var_full_transparent_state;
-  modulo_delta_types = full_transparent_state;
-  modulo_delta_in_merge = None;
+  modulo_delta = st;
+  modulo_delta_types = st;
   check_applied_meta_types = false;
-  resolve_evars = false;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
   frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = true;
-  modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = false
+  modulo_eta = false;
+}
+
+let auto_unif_flags st = {
+  core_unify_flags = auto_core_unif_flags st;
+  merge_unify_flags = auto_core_unif_flags st;
+  subterm_unify_flags = auto_core_unif_flags st;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
 }
 
 let rec eq_constr_mod_evars x y =
@@ -129,12 +134,6 @@ let with_prods nprods poly (c, clenv) f gls =
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 
-let flags_of_state st =
-  {auto_unif_flags with
-    modulo_conv_on_closed_terms = Some st; modulo_delta = st;
-     modulo_delta_types = st;
-     modulo_eta = false}
-
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
     Eauto.registered_e_assumption ::
@@ -156,10 +155,10 @@ and e_my_find_search db_list local_db hdc complete concl =
     List.map_append
       (fun db ->
 	if Hint_db.use_dn db then
-	  let flags = flags_of_state (Hint_db.transparent_state db) in
+	  let flags = auto_unif_flags (Hint_db.transparent_state db) in
 	    List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
 	else
-	  let flags = flags_of_state (Hint_db.transparent_state db) in
+	  let flags = auto_unif_flags (Hint_db.transparent_state db) in
 	    List.map (fun x -> (flags, x)) (Hint_db.map_all hdc db))
       (local_db::db_list)
   in
@@ -760,7 +759,7 @@ let is_ground c gl =
   else tclFAIL 0 (str"Not ground") gl
 
 let autoapply c i gl =
-  let flags = flags_of_state (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
+  let flags = auto_unif_flags (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
   let cty = pf_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
   unify_e_resolve false flags (c,ce) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 2dabe90119..5676a3b58b 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -30,7 +30,7 @@ open Locusops
 
 DECLARE PLUGIN "eauto"
 
-let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
+let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
   if occur_existential t1 || occur_existential t2 then
@@ -148,11 +148,11 @@ and e_my_find_search db_list local_db hdc concl =
   let hintl =
     if occur_existential concl then
       List.map_append (fun db ->
-	let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
+	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
 	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else
       List.map_append (fun db ->
-	let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
+	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
 	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in
   let tac_of_hint =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index de26098745..74fa77e6d2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -41,6 +41,7 @@ open Locus
 open Locusops
 open Misctypes
 open Proofview.Notations
+open Unification
 
 (* Options *)
 
@@ -99,22 +100,27 @@ type conditions =
    -- Eduardo (19/8/97)
 *)
 
+let rewrite_core_unif_flags = {
+  modulo_conv_on_closed_terms = None;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
+  modulo_delta = empty_transparent_state;
+  modulo_delta_types = empty_transparent_state;
+  check_applied_meta_types = true;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = Evar.Set.empty;
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = false;
+  modulo_eta = true;
+}
+
 let rewrite_unif_flags = {
-  Unification.modulo_conv_on_closed_terms = None;
-  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
-  Unification.modulo_delta = empty_transparent_state;
-  Unification.modulo_delta_types = empty_transparent_state;
-  Unification.modulo_delta_in_merge = None;
-  Unification.check_applied_meta_types = true;
-  Unification.resolve_evars = true;
-  Unification.use_pattern_unification = true;
-  Unification.use_meta_bound_pattern_unification = true;
-  Unification.frozen_evars = Evar.Set.empty;
-  Unification.restrict_conv_on_strict_subterms = false;
-  Unification.modulo_betaiota = false;
-  Unification.modulo_eta = true;
-  Unification.allow_K_in_toplevel_higher_order_unification = false
+  core_unify_flags = rewrite_core_unif_flags;
+  merge_unify_flags = rewrite_core_unif_flags;
+  subterm_unify_flags = rewrite_core_unif_flags;
+  allow_K_in_toplevel_higher_order_unification = false;
     (* allow_K does not matter in practice because calls w_typed_unify *)
+  resolve_evars = true
 }
 
 let freeze_initial_evars sigma flags clause =
@@ -127,7 +133,10 @@ let freeze_initial_evars sigma flags clause =
       if Evar.Set.mem evk newevars then evars
       else Evar.Set.add evk evars)
       sigma Evar.Set.empty in
-  { flags with Unification.frozen_evars = evars }
+  {flags with
+    core_unify_flags = {flags.core_unify_flags with frozen_evars = evars};
+    merge_unify_flags = {flags.merge_unify_flags with frozen_evars = evars};
+    subterm_unify_flags = {flags.subterm_unify_flags with frozen_evars = evars}}
 
 let make_flags frzevars sigma flags clause =
   if frzevars then freeze_initial_evars sigma flags clause else flags
@@ -150,7 +159,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in
   let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_unif_flags eqclause in
   let occs =
-    Unification.w_unify_to_subterm_all ~flags env eqclause.evd
+    w_unify_to_subterm_all ~flags env eqclause.evd
       ((if l2r then c1 else c2),concl)
   in List.map try_occ occs
 
@@ -160,33 +169,38 @@ let instantiate_lemma gl c ty l l2r concl =
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
    [eqclause]
 
-let rewrite_conv_closed_unif_flags = {
-  Unification.modulo_conv_on_closed_terms = Some full_transparent_state;
+let rewrite_conv_closed_core_unif_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
     (* We have this flag for historical reasons, it has e.g. the consequence *)
     (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
 
-  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
     (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
     (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
 
-  Unification.modulo_delta = empty_transparent_state;
-  Unification.modulo_delta_types = full_transparent_state;
-  Unification.modulo_delta_in_merge = None;
-  Unification.check_applied_meta_types = true;
-  Unification.resolve_evars = false;
-  Unification.use_pattern_unification = true;
+  modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = true;
+  use_pattern_unification = true;
     (* To rewrite "?n x y" in "y+x=0" when ?n is *)
     (* a preexisting evar of the goal*)
 
-  Unification.use_meta_bound_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
 
-  Unification.frozen_evars = Evar.Set.empty;
+  frozen_evars = Evar.Set.empty;
     (* This is set dynamically *)
 
-  Unification.restrict_conv_on_strict_subterms = false;
-  Unification.modulo_betaiota = false;
-  Unification.modulo_eta = true;
-  Unification.allow_K_in_toplevel_higher_order_unification = false
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = false;
+  modulo_eta = true;
+}
+
+let rewrite_conv_closed_unif_flags = {
+  core_unify_flags = rewrite_conv_closed_core_unif_flags;
+  merge_unify_flags = rewrite_conv_closed_core_unif_flags;
+  subterm_unify_flags = rewrite_conv_closed_core_unif_flags;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
 }
 
 let rewrite_elim with_evars frzevars cls c e =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1d218572da..b23bce8bed 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -529,56 +529,72 @@ let _ =
 let rewrite_transparent_state () =
   Auto.Hint_db.transparent_state (Auto.searchtable_map rewrite_db)
 
-let rewrite_unif_flags = {
+let rewrite_core_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = full_transparent_state;
-  Unification.modulo_delta_in_merge = None;
   Unification.check_applied_meta_types = true;
-  Unification.resolve_evars = false;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
   Unification.frozen_evars = Evar.Set.empty;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
-  Unification.allow_K_in_toplevel_higher_order_unification = true
 }
 
-let rewrite2_unif_flags =
+let rewrite_unif_flags = {
+  Unification.core_unify_flags = rewrite_core_unif_flags;
+  Unification.merge_unify_flags = rewrite_core_unif_flags;
+  Unification.subterm_unify_flags = rewrite_core_unif_flags;
+  Unification.allow_K_in_toplevel_higher_order_unification = true;
+  Unification.resolve_evars = true
+}
+
+let rewrite2_unif_core_flags =
   {  Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
      Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
      Unification.modulo_delta = empty_transparent_state;
      Unification.modulo_delta_types = conv_transparent_state;
-     Unification.modulo_delta_in_merge = None;
      Unification.check_applied_meta_types = true;
-     Unification.resolve_evars = false;
      Unification.use_pattern_unification = true;
      Unification.use_meta_bound_pattern_unification = true;
      Unification.frozen_evars = Evar.Set.empty;
      Unification.restrict_conv_on_strict_subterms = false;
      Unification.modulo_betaiota = true;
      Unification.modulo_eta = true;
-     Unification.allow_K_in_toplevel_higher_order_unification = true
   }
 
-let general_rewrite_unif_flags () = 
+let rewrite2_unif_flags = {
+  Unification.core_unify_flags = rewrite2_unif_core_flags;
+  Unification.merge_unify_flags = rewrite2_unif_core_flags;
+  Unification.subterm_unify_flags = rewrite2_unif_core_flags;
+  Unification.allow_K_in_toplevel_higher_order_unification = true;
+  Unification.resolve_evars = true
+}
+
+let general_rewrite_unif_flags () =
   let ts = rewrite_transparent_state () in
+  let core_flags =
     {  Unification.modulo_conv_on_closed_terms = Some ts;
        Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
        Unification.modulo_delta = ts;
        Unification.modulo_delta_types = ts;
-       Unification.modulo_delta_in_merge = None;
        Unification.check_applied_meta_types = true;
-       Unification.resolve_evars = false;
        Unification.use_pattern_unification = true;
        Unification.use_meta_bound_pattern_unification = true;
        Unification.frozen_evars = Evar.Set.empty;
        Unification.restrict_conv_on_strict_subterms = false;
        Unification.modulo_betaiota = true;
-       Unification.modulo_eta = true;
-       Unification.allow_K_in_toplevel_higher_order_unification = true }
+       Unification.modulo_eta = true }
+  in {
+    Unification.core_unify_flags = core_flags;
+    Unification.merge_unify_flags = core_flags;
+    Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = empty_transparent_state };
+    Unification.allow_K_in_toplevel_higher_order_unification = true;
+    Unification.resolve_evars = true
+  }
+
 
 let refresh_hypinfo env sigma hypinfo =
   let {c=c} = hypinfo in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 35ddc3b388..c5486ce533 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1351,7 +1351,8 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
   Proofview.Goal.nf_enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
+  let flags =
+    if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   let t' = Tacmach.New.pf_get_hyp_typ id gl in
   let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
   let targetid = find_name true (Anonymous,None,t') naming gl in
@@ -4095,12 +4096,15 @@ let admit_as_an_axiom =
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.nf_enter begin fun gl ->
   try
-    let flags =
-      {(default_unify_flags ()) with
-       modulo_delta = state;
-       modulo_delta_types = state;
-       modulo_delta_in_merge = Some state;
-       modulo_conv_on_closed_terms = Some state}
+    let core_flags =
+      { (default_unify_flags ()).core_unify_flags with
+	modulo_delta = state;
+	modulo_conv_on_closed_terms = Some state} in
+    (* What to do on merge and subterm flags?? *)
+    let flags = { (default_unify_flags ()) with
+      core_unify_flags = core_flags;
+      merge_unify_flags = core_flags;
+      subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } }
     in
     let evd = w_unify (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) Reduction.CONV ~flags x y
     in Proofview.V82.tclEVARS evd