aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Init/Prelude.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 5e29f854e8..81268a87ad 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -38,7 +38,7 @@ Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
: dec_int_scope.
(* Parsing / printing of [nat] numbers *)
-Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
+Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001).
(* Printing/Parsing of bytes *)
Export Byte.ByteSyntaxNotations.