An example which failed in 8.5 and that d670c6b6 fixes.

Thanks to Matthieu for the example.

1 files changed, 8 insertions, 3 deletions

diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 4c173a3cd5..1f24ef2a6b 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -170,7 +170,12 @@ Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y)
 
 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.
+
+Instance subrelh : subrelation h (Morphisms.pointwise_relation nat eq).
+Proof. intros x y H; assumption. Qed.
+
+Goal forall a b, h a b -> a 0 = b 0.
 intros.
-rewrite H. (* Fallback on ordinary rewrite without anomaly *)
-Abort.
+setoid_rewrite H. (* Fallback on ordinary rewrite without anomaly *)
+reflexivity.
+Qed.