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.

1 files changed, 1 insertions, 1 deletions

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;
 }