diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-15 12:03:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-16 12:31:54 +0100 |
| commit | d2b7a485963ff079a27e613a178921479fcc6d89 (patch) | |
| tree | 2c2c4dc5112819ee6771e9c3a631f9482913b2d9 | |
| parent | d7691de7184b4cdcfd48fd762011569cde5523c5 (diff) | |
Restricting the need for coqdep_boot to mllib.d files (since ocaml
3.12.1, ocamldep was able to deal with .ml4, so that building .mllib.d
is the only feature that coqdep_boot was still required for).
| -rw-r--r-- | Makefile.build | 12 | ||||
| -rw-r--r-- | tools/coqdep.ml | 1 |
2 files changed, 7 insertions, 6 deletions
diff --git a/Makefile.build b/Makefile.build index c3936c1a7..572ea497d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -1058,19 +1058,19 @@ endif OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4 -checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) @@ -1082,9 +1082,9 @@ checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(SHOW)'COQDEP $<' $(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2e0cce6e5..6d5c02830 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -482,6 +482,7 @@ let coqdep () = if !option_boot then begin add_rec_dir add_known "theories" ["Coq"]; add_rec_dir add_known "plugins" ["Coq"]; + add_caml_dir "tactics"; add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin |