diff options
| author | notin | 2008-04-29 12:33:12 +0000 |
|---|---|---|
| committer | notin | 2008-04-29 12:33:12 +0000 |
| commit | 2ead6184bda0292926dc84834003798a2ae47c19 (patch) | |
| tree | b156422f4f0c77382440ba1ca42f94a20428d255 | |
| parent | 73798a12d39b03e1823b93c1364a86d14e2eec0a (diff) | |
Correction d'un bug dans coq_makefile: génération des règles implicites en présence de l'option -custom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10869 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | tools/coq_makefile.ml4 | 18 |
2 files changed, 14 insertions, 6 deletions
diff --git a/Makefile.build b/Makefile.build index bf5cdc5ada..1a8b90e2fe 100644 --- a/Makefile.build +++ b/Makefile.build @@ -542,7 +542,7 @@ $(GALLINA): $(GALLINACMO) $(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ config/coq_config.cmo tools/coq_makefile.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo $(COQTEX): tools/coq-tex.cmo $(SHOW)'OCAMLC -o $@' diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 0dc91af466..2a5be13d3e 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -161,10 +161,10 @@ let variables l = print "COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ -I $(COQTOP)/library -I $(COQTOP)/parsing \\ -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ - -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\ + -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\ -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \\ -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\ - -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \\ + -I $(COQTOP)/contrib/fourier \\ -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\ -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\ -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\ @@ -183,7 +183,7 @@ let variables l = print "COQDOC:=$(COQBIN)coqdoc\n"; (* Caml executables and relative variables *) printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n"; - printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -c\n"; + printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c\n"; printf "CAMLLINK:=$(CAMLBIN)ocamlc\n"; printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt\n"; print "GRAMMARS:=grammar.cma\n"; @@ -368,8 +368,16 @@ let rec process_cmd_line = function | "-impredicative-set" :: r -> impredicative_set := true; process_cmd_line r | "-custom" :: com :: dependencies :: file :: r -> - some_file := true; - Special (file,dependencies,com) :: (process_cmd_line r) + let check_dep f = + if Filename.check_suffix f ".v" then + some_vfile := true + else if Filename.check_suffix f ".ml" then + some_mlfile := true + else + () + in + List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies); + Special (file,dependencies,com) :: (process_cmd_line r) | "-I" :: d :: r -> Include d :: (process_cmd_line r) | "-R" :: p :: l :: r -> |