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).

7 files changed, 133 insertions, 84 deletions

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