From 2a31e23df8ff0ab67a09008858fa49e77e5f4332 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jan 2020 01:04:07 +0100
Subject: Adding bignat to parse positive numbers; bigint now includes negative
 ints.

Warning: in notations, the name "bigint" actually meant "bignat". A
clarification will eventually be needed.
---
 plugins/syntax/g_numeral.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 49d29e7b63..eccefdf64a 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -29,8 +29,8 @@ let pr_numnot_option = function
 VERNAC ARGUMENT EXTEND numnotoption
   PRINTED BY { pr_numnot_option }
 | [ ] -> { Nop }
-| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft }
-| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n }
+| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning waft }
+| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract n }
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
-- 
cgit v1.2.3