G_prim: the bigint entry keeps numbers in raw strings

4 files changed, 7 insertions, 11 deletions

diff --git a/API/grammar_API.mli b/API/grammar_API.mli
index 44aae771f6..b39ee30b53 100644
--- a/API/grammar_API.mli
+++ b/API/grammar_API.mli
@@ -116,7 +116,7 @@ sig
     val pattern_identref : Names.Id.t located Gram.Entry.e
     val base_ident : Names.Id.t Gram.Entry.e
     val natural : int Gram.Entry.e
-    val bigint : Bigint.bigint Gram.Entry.e
+    val bigint : Constrexpr.raw_natural_number Gram.Entry.e
     val integer : int Gram.Entry.e
     val string : string Gram.Entry.e
     val qualid : API.Libnames.qualid located Gram.Entry.e
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index f2ec6e8b7c..35ffa20d08 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -227,7 +227,7 @@ type prod_info = production_level * production_position
 type (_, _) entry =
 | TTName : ('self, Name.t Loc.located) entry
 | TTReference : ('self, reference) entry
-| TTBigint : ('self, Bigint.bigint) entry
+| TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
@@ -324,10 +324,6 @@ type 'r env = {
 
 let push_constr subst v = { subst with constrs = v :: subst.constrs }
 
-let mkNumeral n =
-  if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
-  else Numeral (Bigint.to_string (Bigint.neg n), false)
-
 let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v ->
 match e with
 | TTConstr _ -> push_constr subst v
@@ -341,8 +337,8 @@ match e with
 | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
   begin match forpat with
-  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (mkNumeral v))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (mkNumeral v))
+  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true)))
   end
 | TTReference ->
   begin match forpat with
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 78f75a73cb..c77d6e204e 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -114,7 +114,7 @@ GEXTEND Gram
   natural:
     [ [ i = INT -> my_int_of_string (!@loc) i ] ]
   ;
-  bigint: (* Negative numbers are dealt with specially *)
-    [ [ i = INT -> (Bigint.of_string i) ] ]
+  bigint: (* Negative numbers are dealt with elsewhere *)
+    [ [ i = INT -> i ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 959e8ddf52..9fb3daabaf 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -199,7 +199,7 @@ module Prim :
     val pattern_identref : Id.t located Gram.entry
     val base_ident : Id.t Gram.entry
     val natural : int Gram.entry
-    val bigint : Bigint.bigint Gram.entry
+    val bigint : Constrexpr.raw_natural_number Gram.entry
     val integer : int Gram.entry
     val string : string Gram.entry
     val lstring : string located Gram.entry