From 1ef6104cf043ec839059cddfe530a81418a3d474 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 7 Jul 2016 13:45:32 +0200
Subject: Add test file for #4880.

---
 test-suite/bugs/closed/4880.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/4880.v

diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v
new file mode 100644
index 0000000000..5569798d54
--- /dev/null
+++ b/test-suite/bugs/closed/4880.v
@@ -0,0 +1,11 @@
+Require Import Coq.Reals.Reals Coq.nsatz.Nsatz.
+Local Open Scope R.
+
+Goal forall x y : R,
+  x*x =  y *  y ->
+  x*x = -y * -y ->
+  x*(x*x) = 0 -> (* The associativity does not actually matter, *)
+  (x*x)*x = 0.   (* just otherwise [assumption] would solve the goal. *)
+Proof.
+  nsatz.
+Qed.
-- 
cgit v1.2.3