From 76ca49c10dc1a5d9cabefd12ea12cc7581ed2eb6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 8 May 2008 18:05:16 +0000 Subject: Oups, my new version of NMake_gen.ml was relying on a 3.10 feature: the very handy Printf.ifprintf was not available on earlier ocaml. This file now uses a very dirty compatibility hack. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10906 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/BigN/NMake_gen.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'theories/Numbers') 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 -- cgit v1.2.3