From d670c6b6ceab80f1c3b6b74ffb53579670c0e621 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 28 Mar 2016 17:53:43 +0200
Subject: Fixing an incorrect use of prod_appvect on a term which was not a
 product in setoid_rewrite.

Before commit e8c47b652, it was raising an error which has been turned
to an anomaly.

This impacted Compcert where the former error was (apparently) caught
so that setoid_rewrite was returning back to ordinary rewrite.
---
 ltac/rewrite.ml                  | 2 +-
 test-suite/success/setoid_test.v | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 20d4651efa..cf2a01052f 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1046,7 +1046,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		      | x -> x
 		    in
 		    let res =
-		      { rew_car = prod_appvect r.rew_car args;
+		      { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
 			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
 			rew_prf = prf; rew_evars = r.rew_evars }
 		    in 
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 0465c4b3fb..4c173a3cd5 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -166,3 +166,11 @@ Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort.
 Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
 Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort.
 
+(* This should not raise an anomaly as it did for some time in early 2016 *)
+
+Definition t := nat -> bool.
+Definition h (a b : t) := forall n, a n = b n.
+Goal forall a b, h a b -> a 0 = true.
+intros.
+rewrite H. (* Fallback on ordinary rewrite without anomaly *)
+Abort.
-- 
cgit v1.2.3