Merge PR#719: Constrexpr.Numeral without bigint

4 files changed, 11 insertions, 11 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 890ce2dec..35ffa20d0 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
@@ -337,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 (Numeral v))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral 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_constr.ml4 b/parsing/g_constr.ml4
index 54bac253d..de7611802 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -203,7 +203,7 @@ GEXTEND Gram
       | c=match_constr -> c
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c.CAst.v with
-              CPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+            | CPrim (Numeral (n,true)) ->
                 CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
@@ -280,7 +280,7 @@ GEXTEND Gram
   atomic_constr:
     [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i)
       | s=sort   -> CAst.make ~loc:!@loc @@  CSort s
-      | n=INT    -> CAst.make ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n))
+      | n=INT    -> CAst.make ~loc:!@loc @@ CPrim (Numeral (n,true))
       | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s)
       | "_"      -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)
       | "?"; "["; id=ident; "]"  -> CAst.make ~loc:!@loc @@  CHole (None, IntroIdentifier id, None)
@@ -395,18 +395,18 @@ GEXTEND Gram
       | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p.CAst.v with
-            | CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+            | CPatPrim (Numeral (n,true)) ->
                  CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p)
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           let p =
             match p with
-            | { CAst.v = CPatPrim (Numeral z) } when Bigint.is_pos_or_zero z ->
+            | { CAst.v = CPatPrim (Numeral (n,true)) } ->
                  CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p
           in
 	  CAst.make ~loc:!@loc @@ CPatCast (p, ty)
-      | n = INT    -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
+      | n = INT    -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (n,true))
       | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ]
   ;
   impl_ident_tail:
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 78f75a73c..c77d6e204 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 959e8ddf5..9fb3daaba 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