diff options
| author | glondu | 2010-07-02 12:54:57 +0000 |
|---|---|---|
| committer | glondu | 2010-07-02 12:54:57 +0000 |
| commit | dacb4b76afe554f1a1e17d981bc98d9fc3a8e807 (patch) | |
| tree | 0c6de9a4f3a7338f32f70520d9647e6f3a356497 /tools | |
| parent | 2de4563cb6192e638df4172c725ec8814e6eb112 (diff) | |
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
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 () = |