diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 171c4ffed..347485eeb 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -28,14 +28,20 @@ let rec gen2 n = if n == 0 then "1" else if n == 1 then "2" let rec genxO n s = if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")" +(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to + /dev/null, but for being compatible with earlier ocaml and not + relying on system-dependent stuff like open_out "/dev/null", + let's use instead a magical hack *) + (* Standard printer, with a final newline *) let pr s = Printf.printf (s^^"\n") -(* /dev/null printer *) -let pn s = Printf.ifprintf stdout s +(* Printing to /dev/null *) +let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) + : ('a, out_channel, unit) format -> 'a) (* Proof printer : prints iff gen_proof is true *) let pp = if gen_proof then pr else pn (* Printer for admitted parts : prints iff gen_proof is false *) -let pa = if gen_proof then pn else pr +let pa = if not gen_proof then pr else pn (* Same as before, but without the final newline *) let pr0 = Printf.printf let pp0 = if gen_proof then pr0 else pn |