From b335fccae5514ef738376354aa619e08bb221d5c Mon Sep 17 00:00:00 2001
From: Andreas Lynge
Date: Sat, 6 Jul 2019 21:17:20 +0200
Subject: Solve universe error with SSR 'rewrite !term'

---
 test-suite/ssr/bang_rewrite.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/ssr/bang_rewrite.v

(limited to 'test-suite')

diff --git a/test-suite/ssr/bang_rewrite.v b/test-suite/ssr/bang_rewrite.v
new file mode 100644
index 0000000000..30e6d57a7a
--- /dev/null
+++ b/test-suite/ssr/bang_rewrite.v
@@ -0,0 +1,13 @@
+Set Universe Polymorphism.
+
+Require Import ssreflect.
+
+Axiom mult@{i} : nat -> nat -> nat.
+Notation "m * n" := (mult m n).
+
+Axiom multA : forall a b c, (a * b) * c = a * (b * c).
+
+(* Previously the following gave a universe error: *)
+
+Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)).
+Proof. by rewrite !multA. Qed.
-- 
cgit v1.2.3