diff options
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | lib/bigint.ml | 6 | ||||
| -rw-r--r-- | lib/bigint.mli | 4 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 2 |
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 = |