Remove dependency to Unix from module Profile

Looking at the source code of Sys.time reveals that it is exactly what
is computed by Profile.get_time. This can also be tested by evaluating:

  Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);;

in an OCaml toplevel with Unix.

This allows to put Profile in grammar.cma without the dependency to
unix.cma while preprocessing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 9 insertions, 14 deletions

diff --git a/CHANGES b/CHANGES
index bd0f4a1346..0e61dd9eb3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -309,10 +309,6 @@ Internal infrastructure
   the ocamlbuild system. In particular "make" takes advantage
   of .mllib files for building .cma/.cmxa. The .vo files to
   compile are now listed in several vo.itarget files.
-- A dependency to Unix has been added to grammar.cma. Compilation of
-  ML files preprocessed with camlp[45] using this library must also
-  load unix.cma. It is recommended to use Makefiles generated by
-  coq_makefile, which handle this transparently.
 
 Changes from V8.1 to V8.2
 =========================
diff --git a/Makefile.build b/Makefile.build
index 6af048572f..adba237537 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -655,7 +655,7 @@ dev/printers.cma: | dev/printers.mllib.d
 parsing/grammar.cma: | parsing/grammar.mllib.d
 	$(SHOW)'Testing $@'
 	@touch test.ml4
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) unix.cma $^ -impl" -impl test.ml4 -o test-grammar
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar
 	@rm -f test-grammar test.*
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
@@ -801,7 +801,7 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)\
 	DEPS=$(CAMLP4DEPS); \
 	if ls $${DEPS} > /dev/null 2>&1; then \
-	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) unix.cma $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \
+	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \
 	else echo $< : Dependency $${DEPS} not ready yet; false; fi
 
 %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
diff --git a/lib/profile.ml b/lib/profile.ml
index d154478177..cde5ed5999 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -15,8 +15,7 @@ let float_of_time t = float_of_int t /. 100.
 let time_of_float f = int_of_float (f *. 100.)
 
 let get_time () =
-  let  {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in
-  time_of_float (ut +. st)
+  time_of_float (Sys.time ())
 
 (* Since ocaml 3.01, gc statistics are in float *)
 let get_alloc () =
@@ -155,7 +154,10 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
 (* Unix measure of time is approximative and shoitt delays are often
    unperceivable; therefore, total times are measured in one (big)
    step to avoid rounding errors and to get the best possible
-   approximation *)
+   approximation.
+   Note: Sys.time is the same as:
+     Unix.(let x = times () in x.tms_utime +. x.tms_stime)
+ *)
 
 (*
 ----------        start profile for f1
diff --git a/lib/profile.mli b/lib/profile.mli
index 5bcebfb0dd..56f78cba8a 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -8,12 +8,9 @@
 
 (** {6 This program is a small time and allocation profiler for Objective Caml } *)
 
-(*i It requires the UNIX library *)
-
 (** Adapted from Christophe Raffalli *)
 
-(** To use it, link it with the program you want to profile (do not forget
-"-cclib -lunix -custom unix.cma" among the link options).
+(** To use it, link it with the program you want to profile.
 
 To trace a function "f" you first need to get a key for it by using :
 
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 20ec649f09..6565a6c23f 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -288,7 +288,7 @@ let variables defs =
     print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
     print "CAMLP4OPTIONS:=\n";
     List.iter var_aux defs;
-    print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) unix.cma -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n";
+    print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n";
     print "\n"
 
 let parameters () =