From 34f8872ba83aa5e91d73a80034b4c58db25dbbf7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 31 Jan 2019 14:08:30 -0500
Subject: Fix off-by-one error in nat syntax warnings

Fixes #9453
---
 theories/Init/Prelude.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

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.
-- 
cgit v1.2.3