Index: otherlibs/win32unix/unix.ml
===================================================================
--- otherlibs/win32unix/unix.ml	(revision 11888)
+++ otherlibs/win32unix/unix.ml	(working copy)
@@ -408,9 +408,7 @@ external localtime : float -> tm = "unix
 external mktime : tm -> float * tm = "unix_mktime"
 let alarm n = invalid_arg "Unix.alarm not implemented"
 external sleep : int -> unit = "unix_sleep"
-let times () =
-  { tms_utime = Sys.time(); tms_stime = 0.0;
-    tms_cutime = 0.0; tms_cstime = 0.0 }
+external times: unit -> process_times = "unix_times"
 external utimes : string -> float -> float -> unit = "unix_utimes"
 
 type interval_timer =
Index: otherlibs/win32unix/Makefile.nt
===================================================================
--- otherlibs/win32unix/Makefile.nt	(revision 11888)
+++ otherlibs/win32unix/Makefile.nt	(working copy)
@@ -21,7 +21,7 @@ WIN_FILES = accept.c bind.c channels.c c
   mkdir.c open.c pipe.c read.c rename.c \
   select.c sendrecv.c \
   shutdown.c sleep.c socket.c sockopt.c startup.c stat.c \
-  system.c unixsupport.c windir.c winwait.c write.c \
+  system.c times.c unixsupport.c windir.c winwait.c write.c \
   winlist.c winworker.c windbug.c
 
 # Files from the ../unix directory
Index: otherlibs/win32unix/times.c
===================================================================
--- otherlibs/win32unix/times.c	(revision 0)
+++ otherlibs/win32unix/times.c	(revision 0)
@@ -0,0 +1,35 @@
+#include <windows.h>
+#include <mlvalues.h>
+#include "unixsupport.h"
+
+
+double to_sec(FILETIME ft) {
+  ULARGE_INTEGER tmp;
+
+  tmp.u.LowPart = ft.dwLowDateTime;
+  tmp.u.HighPart = ft.dwHighDateTime;
+
+  /* convert to seconds:
+     GetProcessTimes returns number of 100-nanosecond intervals */
+  return tmp.QuadPart / 1e7;
+}
+
+
+value unix_times(value unit) {
+
+  value res;
+  FILETIME creation, exit, stime, utime;
+
+  if (!(GetProcessTimes(GetCurrentProcess(), &creation, &exit, &stime, &utime))) {
+    win32_maperr(GetLastError());
+    uerror("times", Nothing);
+  }
+
+  res = alloc_small(4 * Double_wosize, Double_array_tag);
+  Store_double_field(res, 0, to_sec(utime));
+  Store_double_field(res, 1, to_sec(stime));
+  Store_double_field(res, 2, 0);
+  Store_double_field(res, 3, 0);
+  return res;
+
+}