From 91c2a866e7827c0ede0539cb49f924b68db569a9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Nov 2014 15:28:19 +0100
Subject: 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).
---
 proofs/clenvtac.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 7d25bb6659..087ac0c334 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -96,6 +96,7 @@ let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
 let fail_quick_core_unif_flags = {
   modulo_conv_on_closed_terms = Some full_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 = full_transparent_state;
   check_applied_meta_types = false;
-- 
cgit v1.2.3