From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 test-suite/success/rewrite_in.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/success/rewrite_in.v

(limited to 'test-suite/success/rewrite_in.v')

diff --git a/test-suite/success/rewrite_in.v b/test-suite/success/rewrite_in.v
new file mode 100644
index 00000000..29fe915f
--- /dev/null
+++ b/test-suite/success/rewrite_in.v
@@ -0,0 +1,8 @@
+Require Import Setoid.
+
+Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True.
+  intros P Q f p H.
+  rewrite H in p || trivial.
+Qed.
+
+
-- 
cgit v1.2.3