From 44638cda2f8f7461506a6e5a9a2edf860971f96c Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 12 Mar 2018 17:21:04 +0100
Subject: Decimal: scope name changed dec_(u)int_scope

 This avoid a clash with int_scope in ssreflect's ssrint.v
---
 theories/Init/Decimal.v | 8 ++++----
 theories/Init/Prelude.v | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 34b4e75814..1ff00ec11c 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -42,10 +42,10 @@ Notation zero := (D0 Nil).
 
 Inductive int := Pos (d:uint) | Neg (d:uint).
 
-Delimit Scope uint_scope with uint.
-Bind Scope uint_scope with uint.
-Delimit Scope int_scope with int.
-Bind Scope int_scope with int.
+Delimit Scope dec_uint_scope with uint.
+Bind Scope dec_uint_scope with uint.
+Delimit Scope dec_int_scope with int.
+Bind Scope dec_int_scope with int.
 
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e8997d30b8..6d98bcb34a 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -28,12 +28,12 @@ Declare ML Module "ground_plugin".
 Declare ML Module "numeral_notation_plugin".
 
 (* Parsing / printing of decimal numbers *)
-Arguments Nat.of_uint d%uint_scope.
-Arguments Nat.of_int d%int_scope.
+Arguments Nat.of_uint d%dec_uint_scope.
+Arguments Nat.of_int d%dec_int_scope.
 Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
-  : uint_scope.
+  : dec_uint_scope.
 Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
-  : int_scope.
+  : dec_int_scope.
 
 (* Parsing / printing of [nat] numbers *)
 Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
-- 
cgit v1.2.3