diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:27 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:27 +0000 |
| commit | 0270ae316d7e9d6ddb060383d24d852c54f067d6 (patch) | |
| tree | 3f452f730868b0b61d69c13419e227aeeb0a0abb /theories/Numbers/Natural/BigN/NMake_gen.ml | |
| parent | bf69f9e2204de87a08ef2cc622d347b33f3f42ce (diff) | |
Discontinue support for ocaml 3.09.*
Ocaml 3.10.0 is already three year old...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 20cb01b16..0c15950ed 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -34,16 +34,10 @@ let rec iter_name i j base sep = if i >= j then base^(string_of_int i) else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j) -(* 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") (* Printing to /dev/null *) -let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) - : ('a, out_channel, unit) format -> 'a) +let pn s = Printf.ifprintf stdout s (* 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 *) |