diff options
| author | notin | 2008-02-28 15:40:57 +0000 |
|---|---|---|
| committer | notin | 2008-02-28 15:40:57 +0000 |
| commit | 85302f651dba5b8577d0ff9ec5998a4e97f7731c (patch) | |
| tree | 964b2c76a7b3d5d5d417368ef4a03d0ff613f1d1 /tools | |
| parent | b8afd9fbeac384944ccfc36cb449409eb151510e (diff) | |
Coq_makefile: correction de l'appel aux exécutables Ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 7e277e3ed8..88f967d266 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -123,7 +123,7 @@ let standard sds sps = print "\n\n" let includes () = - if !some_vfile then print "include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n" + if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n" let implicit () = let ml_rules () = @@ -168,8 +168,8 @@ let variables l = | _ :: r -> var_aux r in section "Variables definitions."; - print "CAMLP4LIB:=$(shell camlp5 -where 2> /dev/null || camlp4 -where)\n"; - print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; + printf "CAMLP4LIB:=%s\n" Coq_config.camlp4lib; + printf "CAMLP4:=%s\n" (Filename.concat Coq_config.camldir Coq_config.camlp4); print "COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ -I $(COQTOP)/library -I $(COQTOP)/parsing \\ -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ @@ -187,15 +187,17 @@ let variables l = else print "OPT:=\n"; if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; + (* Coq executables and relative variables *) print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQC:=$(COQBIN)coqc\n"; + print "COQDEP:=$(COQBIN)coqdep -c\n"; print "GALLINA:=$(COQBIN)gallina\n"; print "COQDOC:=$(COQBIN)coqdoc\n"; - print "CAMLC:=ocamlc -rectypes -c\n"; - print "CAMLOPTC:=ocamlopt -c\n"; - print "CAMLLINK:=ocamlc\n"; - print "CAMLOPTLINK:=ocamlopt\n"; - print "COQDEP:=$(COQBIN)coqdep -c\n"; + (* Caml executables and relative variables *) + printf "CAMLC:=%s/ocamlc -rectypes -c\n" Coq_config.camldir; + printf "CAMLOPTC:=%s/ocamlopt -c\n" Coq_config.camldir; + printf "CAMLLINK:=%s/ocamlc\n" Coq_config.camldir; + printf "CAMLOPTLINK:=%s/ocamlopt\n" Coq_config.camldir; print "GRAMMARS:=grammar.cma\n"; print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; print "PP:=-pp \"$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; |