diff options
| author | mdenes | 2013-01-22 14:18:38 +0000 |
|---|---|---|
| committer | mdenes | 2013-01-22 14:18:38 +0000 |
| commit | 62ce65dadb0afb8815b26069246832662846c7ec (patch) | |
| tree | 12d463433d64263510f3875b116f7b8cf16d43bc /tools | |
| parent | e88df65bbc64b18da34a4233f680829025ca76d9 (diff) | |
Revert "remove -rectypes except for term.ml"
Preparing landing of the native compiler, which requires -rectypes flag.
This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index c3261c1a79..060bd3d373 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -409,12 +409,12 @@ let variables is_install opt (args,defs) = -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\ -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)grammar\""; 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\n"; - print "CAMLOPTC?=$(OCAMLOPT) -c\n"; - print "CAMLLINK?=$(OCAMLC)\n"; - print "CAMLOPTLINK?=$(OCAMLOPT)\n"; + -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 "GRAMMARS?=grammar.cma\n"; print "ifeq ($(CAMLP4),camlp5) CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo @@ -610,9 +610,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 -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; - print "\t$(OCAMLDOC) -latex -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; end; if !some_vfile then begin |