From 9285bf164e0e9723b482d668f52ec6363623383c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Nov 2017 22:04:55 +0100
Subject: Fixing a 8.7 regression of ring_simplify in ArithRing.

With help from Guillaume (see discussion at
https://github.com/coq/coq/issues/6191).
---
 test-suite/bugs/closed/6191.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test-suite/bugs/closed/6191.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/6191.v b/test-suite/bugs/closed/6191.v
new file mode 100644
index 0000000000..e0d912509b
--- /dev/null
+++ b/test-suite/bugs/closed/6191.v
@@ -0,0 +1,16 @@
+(* Check a 8.7.1 regression in ring_simplify *)
+
+Require Import ArithRing BinNat.
+Goal forall f x, (2+x+f (N.to_nat 2)+3=4).
+intros.
+ring_simplify (2+x+f (N.to_nat 2)+3).
+match goal with |- x + f (N.to_nat 2) + 5 = 4 => idtac end.
+Abort.
+
+Require Import ZArithRing BinInt.
+Open Scope Z_scope.
+Goal forall x, (2+x+3=4).
+intros.
+ring_simplify (2+x+3).
+match goal with |- x+5 = 4 => idtac end.
+Abort.
-- 
cgit v1.2.3