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

---
 plugins/syntax/numeral.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 2db76719b8..fbf43be91f 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -64,7 +64,7 @@ let locate_numeral () =
   let hex = "num.hexadecimal.type" in
   let int = "num.num_int.type" in
   let uint = "num.num_uint.type" in
-  let num = "num.numeral.type" in
+  let num = "num.number.type" in
   if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec
      && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex
      && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num
-- 
cgit v1.2.3