diff options
| author | letouzey | 2012-10-06 10:08:42 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:42 +0000 |
| commit | f975575187d0a19e7cc1afc43459a92eeb12b3f1 (patch) | |
| tree | 97d9c364c13ba82b6bfbafea40bbc5b040590c32 /tools | |
| parent | d2fd26a0ac600d066e79df4ab33b9bc924de069d (diff) | |
remove -rectypes except for term.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 3b2c63b0fa..88ffb14ab0 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -410,10 +410,10 @@ let variables is_install opt (args,defs) = List.iter (fun c -> print " \\ -I $(COQLIB)/"; print c) Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; - print "CAMLC?=$(OCAMLC) -c -rectypes\n"; - print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n"; - print "CAMLLINK?=$(OCAMLC) -rectypes\n"; - print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n"; + print "CAMLC?=$(OCAMLC) -c\n"; + print "CAMLOPTC?=$(OCAMLOPT) -c\n"; + print "CAMLLINK?=$(OCAMLC)\n"; + print "CAMLOPTLINK?=$(OCAMLOPT)\n"; print "GRAMMARS?=grammar.cma\n"; print "ifeq ($(CAMLP4),camlp5) CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo @@ -604,9 +604,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other begin print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; print "\t mkdir $@ || rm -rf $@/*\n"; - print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLDOC) -html -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; - print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLDOC) -latex -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; end; if !some_vfile then begin |