From 55ce331822a673d710451c628ec5a731ab36da1f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 2 Feb 2016 15:28:48 +0100
Subject: Fix bug #4544: Backtrack on using full betaiota reduction during
 keyed unification.

---
 tactics/equality.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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