From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 plugins/setoid_ring/ArithRing.v | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

(limited to 'plugins/setoid_ring/ArithRing.v')

diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 5f5b9792..bb1eca49 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Import Mult.
@@ -41,9 +43,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 +57,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]).
 
-- 
cgit v1.2.3