Passage d'une bibliothèque de grands entiers naturels vers une bibliothèques de grands entiers relatifs munis des 4 opérations de base

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

7 files changed, 11 insertions, 11 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
index b54c3323b7..60e16e7094 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -11,7 +11,7 @@
 (*i*)
 open Util
 open Pp
-open Bignat
+open Bigint
 open Names
 open Nametab
 open Libnames
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 5760f7c27a..e803d65e7c 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -11,7 +11,7 @@
 (*i*)
 open Util
 open Pp
-open Bignat
+open Bigint
 open Names
 open Nametab
 open Libnames
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c483327b64..56e2171e95 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -483,7 +483,7 @@ type cases_pattern_expr =
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_expr list
-  | CPatNumeral of loc * Bignat.bigint
+  | CPatNumeral of loc * Bigint.bigint
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
@@ -512,7 +512,7 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr
   | CNotation of loc * notation * constr_expr list
-  | CNumeral of loc * Bignat.bigint
+  | CNumeral of loc * Bigint.bigint
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index a3224128a8..152a54dc01 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -77,7 +77,7 @@ type cases_pattern_expr =
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_expr list
-  | CPatNumeral of loc * Bignat.bigint
+  | CPatNumeral of loc * Bigint.bigint
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
@@ -106,7 +106,7 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr
   | CNotation of loc * notation * constr_expr list
-  | CNumeral of loc * Bignat.bigint
+  | CNumeral of loc * Bigint.bigint
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index d73e80f749..3acf6904b2 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -93,7 +93,7 @@ let make_act (f : loc -> constr_expr action_env -> constr_expr) pil =
         Gramext.action (fun (v:identifier) ->
 	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
-        Gramext.action (fun (v:Bignat.bigint) ->
+        Gramext.action (fun (v:Bigint.bigint) ->
 	  make ((p,CNumeral (dummy_loc,v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:constr_expr list) ->
@@ -119,7 +119,7 @@ let make_act_in_cases_pattern (* For Notations *)
         Gramext.action (fun (v:identifier) ->
 	  make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
-        Gramext.action (fun (v:Bignat.bigint) ->
+        Gramext.action (fun (v:Bigint.bigint) ->
 	  make ((p,CPatNumeral (dummy_loc,v)) :: env) tl)
     | Some (p, ETConstrList _) :: tl ->
         Gramext.action (fun (v:cases_pattern_expr list) ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1d7b8345f3..9963bad73a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -113,7 +113,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 bigint : Bigint.bigint Gram.Entry.e
     val integer : int Gram.Entry.e
     val string : string Gram.Entry.e
     val qualid : qualid located Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4e1f01c62d..c76de59f14 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -222,7 +222,7 @@ let rec pr_cases_pattern _inh = function
   | CPatNotation (_,"( _ )",[p]) ->
       str"("++ pr_cases_pattern _inh p ++ str")"
   | CPatNotation (_,s,env) -> fst (pr_patnotation pr_cases_pattern s env)
-  | CPatNumeral (_,n) -> Bignat.pr_bigint n
+  | CPatNumeral (_,n) -> Bigint.pr_bigint n
   | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_cases_pattern _inh p)
 
 let pr_cases_pattern = pr_cases_pattern (0,E) (* level unused *)
@@ -320,7 +320,7 @@ let rec pr inherited a =
   | CNotation (_,"( _ )",[t]) ->
       str"("++ pr (max_int,E) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation pr s env
-  | CNumeral (_,p) -> Bignat.pr_bigint p, latom
+  | CNumeral (_,p) -> Bigint.pr_bigint p, latom
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom
   | CDynamic _ -> str "<dynamic>", latom
   in