From a5ae3b2856e6cc6683652a0abb5a84b9787527c0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 9 Mar 2016 15:15:38 +0100
Subject: Fix strategy of Keyed Unification

Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 80f6038cb7..f72a72f46d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -228,7 +228,7 @@ let rewrite_keyed_core_unif_flags = {
     (* This is set dynamically *)
 
   restrict_conv_on_strict_subterms = false;
-  modulo_betaiota = false;
+  modulo_betaiota = true;
 
   modulo_eta = true;
 }
-- 
cgit v1.2.3