Ajout d'une entre Prim.bigint

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3332 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 8 insertions, 1 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index f65ebd64d7..9dd073cfd6 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -69,7 +69,7 @@ ifdef Quotify then
 open Q
 
 GEXTEND Gram
-  GLOBAL: ident natural integer string preident ast
+  GLOBAL: ident natural integer bigint string preident ast
     astlist qualid reference dirpath identref name base_ident var;
 
  (* Compatibility: Prim.var is a synonym of Prim.ident *)
@@ -97,6 +97,10 @@ GEXTEND Gram
   natural:
     [ [ i = INT -> local_make_posint i ] ]
   ;
+  bigint:
+    [ [ i = INT -> Bignat.POS (Bignat.of_string i)
+      | "-"; i = INT -> Bignat.NEG (Bignat.of_string i) ] ]
+  ;
   integer:
     [ [ i = INT      -> local_make_posint i
       | "-"; i = INT -> local_make_negint i ] ]
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 632c7983ac..9a6caf41d7 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -309,6 +309,7 @@ module Prim =
     let ident = gec_gen rawwit_ident "ident"
     let natural = gec_gen rawwit_int "natural"
     let integer = gec_gen rawwit_int "integer"
+    let bigint = Gram.Entry.create "Prim.bigint"
     let string = gec_gen rawwit_string "string"
     let reference = make_gen_entry uprim rawwit_ref "reference"
 
@@ -524,6 +525,7 @@ let compute_entry allow_create adjust = function
   | ETConstr (9,_) -> weaken_entry Constr.constr9, None
   | ETConstr (n,q) -> weaken_entry Constr.constr, adjust (n,q)
   | ETIdent -> weaken_entry Constr.ident, None
+  | ETBigint -> weaken_entry Prim.bigint, None
   | ETReference -> weaken_entry Constr.global, None
   | ETPattern -> weaken_entry Constr.pattern, None
   | ETOther (u,n) ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 467fe5f331..c185c9309e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -111,6 +111,7 @@ module Prim :
     val identref : identifier located Gram.Entry.e
     val base_ident : identifier Gram.Entry.e
     val natural : int Gram.Entry.e
+    val bigint : Bignat.bigint Gram.Entry.e
     val integer : int Gram.Entry.e
     val string : string Gram.Entry.e
     val qualid : qualid located Gram.Entry.e