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(-)

(limited to 'tactics')

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


From db2c6f0054d3e05f82da7494ce790c04b1976401 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 28 Feb 2016 13:19:47 +0100
Subject: Fixing bug #4596: [rewrite] broke in the past few weeks.

Checking that a term was indeed a relation was made too early, as the
decomposition function recognized relations of the form "f (g .. (h x y))
with f, g unary and only h binary. We postpone this check to the very end.
---
 tactics/rewrite.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 5ca74050a1..803e187ff5 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -468,11 +468,15 @@ let rec decompose_app_rel env evd t =
     let len = Array.length args in
     let fargs = Array.sub args 0 (Array.length args - 2) in
     let rel = mkApp (f, fargs) in
-    let ty = Retyping.get_type_of env evd rel in
-    let () = if not (Reduction.is_arity env ty) then error_no_relation () in
     rel, args.(len - 2), args.(len - 1)
   | _ -> error_no_relation ()
 
+let decompose_app_rel env evd t =
+  let (rel, t1, t2) = decompose_app_rel env evd t in
+  let ty = Retyping.get_type_of env evd rel in
+  let () = if not (Reduction.is_arity env ty) then error_no_relation () in
+  (rel, t1, t2)
+
 let decompose_applied_relation env sigma (c,l) =
   let ctype = Retyping.get_type_of env sigma c in
   let find_rel ty =
-- 
cgit v1.2.3