diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-20 22:04:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-23 12:52:29 +0100 |
| commit | 9285bf164e0e9723b482d668f52ec6363623383c (patch) | |
| tree | 0b1f0af85afffa93c47f8df56c0d3bca2f4b9d5d /test-suite | |
| parent | 22ae762fa8940028f6a3d8a5fd4147d5ca3b53b9 (diff) | |
Fixing a 8.7 regression of ring_simplify in ArithRing.
With help from Guillaume (see discussion at
https://github.com/coq/coq/issues/6191).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/6191.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/6191.v b/test-suite/bugs/closed/6191.v new file mode 100644 index 000000000..e0d912509 --- /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. |