Follow up to experimental eager evar unification in bcba6d1bc9:

Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).

2 files changed, 8 insertions, 3 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a6b02bcf9..982b8a3ec 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -234,6 +234,8 @@ type core_unify_flags = {
     (* This refinement of the conversion on closed terms is activable *)
     (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *)
 
+  use_evars_eagerly_in_conv_on_closed_terms : bool;
+
   modulo_delta : Names.transparent_state;
     (* This controls which constants are unfoldable; this is on for apply *)
     (* (but not simple apply) since Feb 2008 for 8.2 *)
@@ -299,6 +301,7 @@ 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;
+  use_evars_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = ts;
   modulo_delta_types = ts;
   check_applied_meta_types = true;
@@ -509,10 +512,10 @@ let isAllowedEvar flags c = match kind_of_term c with
   | _ -> false
 
 let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN =
-  match subst_defined_metas_evars (metasubst,evarsubst) tyM with
+  match subst_defined_metas_evars (metasubst,[]) tyM with
   | None -> sigma
   | Some m ->
-  match subst_defined_metas_evars (metasubst,evarsubst) tyN with
+  match subst_defined_metas_evars (metasubst,[]) tyN with
   | None -> sigma
   | Some n ->
     if is_ground_term sigma m && is_ground_term sigma n then
@@ -844,7 +847,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       match flags.modulo_conv_on_closed_terms with
       | None -> None
       | Some convflags ->
-      let subst = if flags.use_metas_eagerly_in_conv_on_closed_terms then (metasubst,evarsubst) else (ms,es) in
+      let subst = ((if flags.use_metas_eagerly_in_conv_on_closed_terms then metasubst else ms), (if flags.use_evars_eagerly_in_conv_on_closed_terms then evarsubst else es)) in
       match subst_defined_metas_evars subst cM with
       | None -> (* some undefined Metas in cM *) None
       | Some m1 ->
@@ -1371,6 +1374,7 @@ 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;
+  use_evars_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = ts;
   check_applied_meta_types = true;
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0f5a62bb5..ce74852d3 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -13,6 +13,7 @@ open Evd
 type core_unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly_in_conv_on_closed_terms : bool;
+  use_evars_eagerly_in_conv_on_closed_terms : bool;
   modulo_delta : Names.transparent_state;
   modulo_delta_types : Names.transparent_state;
   check_applied_meta_types : bool;