Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 22 insertions, 7 deletions

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]).