Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing

2 files changed, 32 insertions, 3 deletions

diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 447acb9057..8e4d8b0d34 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -41,9 +41,12 @@ Ltac Ss_to_add f acc :=
   | _ => constr:((acc + f)%nat)
   end.
 
+(* For internal use only *)
+Local Definition protected_to_nat := N.to_nat.
+
 Ltac natprering :=
   match goal with
-    |- context C [S ?p] =>
+  |- context C [S ?p] =>
     match p with
       O => fail 1 (* avoid replacing 1 with 1+0 ! *)
     | p => match isnatcst p with
@@ -52,9 +55,19 @@ Ltac natprering :=
                          fold v; natprering
            end
     end
-  | _ => idtac
+  | _ => change N.to_nat with protected_to_nat
+  end.
+
+Ltac natpostring :=
+  match goal with
+  | |- context [N.to_nat ?x] =>
+    let v := eval cbv in (N.to_nat x) in
+    change (N.to_nat x) with v;
+    natpostring
+  | _ => change protected_to_nat with N.to_nat
   end.
 
 Add Ring natr : natSRth
-  (morphism nat_morph_N, constants [natcst], preprocess [natprering]).
+  (morphism nat_morph_N, constants [natcst],
+   preprocess [natprering], postprocess [natpostring]).
 
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.