From 31aa17efa51c6420f2b2f8fdb1e8397ab5212cbb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Nov 2014 18:10:14 +0100
Subject: Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags
 too. This allows to have the example in test setoid_unif.v to work again.

---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 3c34c507f4..22145d4615 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -531,7 +531,7 @@ let rewrite_transparent_state () =
 let rewrite_core_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
-  Unification.use_evars_eagerly_in_conv_on_closed_terms = false;
+  Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = full_transparent_state;
   Unification.check_applied_meta_types = true;
-- 
cgit v1.2.3