1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 9629b213..86e55922 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -17,3 +17,24 @@ 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.
+
+(* Behavior of rewrite wrt conversion *)
+
+Require Import Arith.
+
+Goal forall n, 0 + n = n -> True.
+intros n H.
+rewrite plus_0_l in H.
+Abort.