diff options
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/Makefile.dev b/Makefile.dev index 8f7d21694..ea1a3d40a 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,7 +15,7 @@ # Debug printers in dev/ ######################### -.PHONY: devel printers +.PHONY: devel printers camldevfiles DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo @@ -85,13 +85,27 @@ endif # But these partial targets could be quite handy for quick builds # of specific components of Coq. +########################################################################### +# OCaml dev files +########################################################################### +camldevfiles: $(MERLINFILES) META.coq + +.merlin: .merlin.in + cp -a "$<" "$@" + +%/.merlin: %/.merlin.in + cp -a "$<" "$@" + +META.coq: META.coq.in + cp -a "$<" "$@" + ############################### ### 1) general-purpose targets ############################### coqlight: theories-light tools coqbinaries -states: theories/Init/Prelude.vo +states: camldevfiles theories/Init/Prelude.vo miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte @@ -174,7 +188,6 @@ MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) -FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO)) FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) @@ -188,7 +201,6 @@ micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) setoid_ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) -fourier: $(FOURIERVO) $(FOURIERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) rtauto: $(RTAUTOVO) $(RTAUTOCMO) @@ -196,7 +208,7 @@ btauto: $(BTAUTOVO) $(BTAUTOCMO) ltac: $(LTACVO) $(LTACCMO) .PHONY: omega micromega setoid_ring nsatz extraction -.PHONY: fourier funind cc rtauto btauto ltac +.PHONY: funind cc rtauto btauto ltac # For emacs: # Local Variables: |