1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 86e55922df..b06718251e 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -38,3 +38,33 @@ Goal forall n, 0 + n = n -> True.
 intros n H.
 rewrite plus_0_l in H.
 Abort.
+
+(* Dependent rewrite from left-to-right *)
+
+Lemma l1 :
+  forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
+intros x y H P H0.
+rewrite H.
+rewrite H in H0.
+assumption.
+Qed.
+
+(* Dependent rewrite from right-to-left *)
+
+Lemma l2 :
+  forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
+intros x y H P H0.
+rewrite <- H.
+rewrite <- H in H0.
+assumption.
+Qed.
+
+(* Check dependent rewriting with non-symmetric equalities *)
+
+Lemma l3:forall x (H:eq_true x) (P:forall x, eq_true x -> Type), P x H -> P x H.
+intros x H P H0.
+rewrite H.
+rewrite H in H0.
+assumption.
+Qed.
+