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.
---
 vernac/egramcoq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 1d790e7cd2..6f8ee76b33 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -368,7 +368,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl))
 | TTName -> MayRecNo (Aentry Prim.name)
 | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
-| TTBigint -> MayRecNo (Aentry Prim.bigint)
+| TTBigint -> MayRecNo (Aentry Prim.bignat)
 | TTReference -> MayRecNo (Aentry Constr.global)
 
 let interp_entry forpat e = match e with
-- 
cgit v1.2.3