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.

2 files changed, 20 insertions, 2 deletions

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 =
diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v
new file mode 100644
index 0000000000..592fdb6580
--- /dev/null
+++ b/test-suite/bugs/closed/4596.v
@@ -0,0 +1,14 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+
+Definition T (x : bool) := x = true.
+
+Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat)
+  (s : forall n : nat, bool)
+  (s0 s1 : nat -> S -> S),
+  (forall (str0 : S) (n m : nat),
+  (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) ->
+    T (b str0 m)) ->
+  T (b str p).
+Proof.
+intros ???????? H0.
+rewrite H0.