From e3968a275532d40009f4ed0e7ea8abbe783e034f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 4 Dec 2020 07:46:21 +0100
Subject: Add checks for invalid occurrences in setoid rewrite.

We additionally check that occurrence 0 is invalid in simpl at,
unfold at, etc.
---
 test-suite/success/rewrite_in.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/rewrite_in.v b/test-suite/success/rewrite_in.v
index 29fe915ff4..3433866239 100644
--- a/test-suite/success/rewrite_in.v
+++ b/test-suite/success/rewrite_in.v
@@ -5,4 +5,10 @@ Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True.
   rewrite H in p || trivial.
 Qed.
 
-
+Goal 1 = 0 -> 0 = 1.
+  intro H.
+  Fail rewrite H at 1 2 3. (* bug #13566 *)
+  Fail rewrite H at 0.
+  rewrite H at 1.
+  reflexivity.
+Qed.
-- 
cgit v1.2.3