1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 9629b2132..a11297ea9 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -17,3 +17,15 @@ intros n n' l l'.
  dependent rewrite (ax n n' l l').
 split; reflexivity.
 Qed.
+
+(* Used to raise an anomaly instead of an error in 8.1 *)
+(* Submitted by Y. Makarov *)
+
+Parameter N : Set.
+Parameter E : N -> N -> Prop.
+
+Axiom e : forall (A : Set) (EA : A -> A -> Prop) (a : A), EA a a.
+
+Theorem th : forall x : N, E x x.
+intro x. try rewrite e.
+Abort.