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

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