From 2d44c8246eccba7c1c452cbfbc6751cd222d0a6a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 12 Sep 2020 09:10:26 +0200
Subject: Renaming Numeral.v into Number.v

---
 theories/Numbers/AltBinNotations.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index 7c846571a7..c203c178f5 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -17,7 +17,7 @@
     the [Decimal.int] representation. When working with numbers with
     thousands of digits and more, conversion from/to [Decimal.int] can
     become significantly slow. If that becomes a problem for your
-    development, this file provides some alternative [Numeral
+    development, this file provides some alternative [Number
     Notation] commands that use [Z] as bridge type. To enable these
     commands, just be sure to [Require] this file after other files
     defining numeral notations.
-- 
cgit v1.2.3