Bigint: avoid dependency over Pp

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

5 files changed, 3 insertions, 13 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 570ad59ff..d0b358d8e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -64,7 +64,7 @@ let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string
 
 let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
-let ppbigint n = pp (Bigint.pr_bigint n);;
+let ppbigint n = pp (str (Bigint.to_string n));;
 
 let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
 let ppintset l = pp (prset int (Intset.elements l))
diff --git a/interp/notation.ml b/interp/notation.ml
index b93ad6bcc..a088f9f8e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -383,7 +383,7 @@ let interp_prim_token_gen g loc p local_scopes =
   with Not_found ->
     user_err_loc (loc,"interp_prim_token",
     (match p with
-      | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
+      | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token =
diff --git a/lib/bigint.ml b/lib/bigint.ml
index 7fce6b815..1985eceb8 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -6,10 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i*)
-open Pp
-(*i*)
-
 (***************************************************)
 (* Basic operations on (unbounded) integer numbers *)
 (***************************************************)
@@ -348,8 +344,6 @@ let is_strictly_pos n = is_strictly_pos (ints_of_z n)
 let is_neg_or_zero n = is_neg_or_zero (ints_of_z n)
 let is_pos_or_zero n = is_pos_or_zero (ints_of_z n)
 
-let pr_bigint n = str (to_string n)
-
 (* spiwack: computes n^m *)
 (* The basic idea of the algorithm is that n^(2m) = (n^2)^m *)
 (* In practice the algorithm performs :
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 92a97bdc8..34bc8e40f 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-
 (** Arbitrary large integer numbers *)
 
 type bigint
@@ -39,5 +37,3 @@ val is_neg_or_zero : bigint -> bool
 val neg : bigint -> bigint
 
 val pow : bigint -> bigint -> bigint
-
-val pr_bigint : bigint -> std_ppcmds
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index bdf69c9cf..38f5fc1c6 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,7 +151,7 @@ let pr_or_var pr = function
   | ArgVar (loc,s) -> pr_lident (loc,s)
 
 let pr_prim_token = function
-  | Numeral n -> Bigint.pr_bigint n
+  | Numeral n -> str (Bigint.to_string n)
   | String s -> qs s
 
 let pr_evar pr n l =