diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 27 | ||||
| -rw-r--r-- | tools/coqdep.ml | 4 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 2 |
3 files changed, 22 insertions, 11 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 4372ac72ae..f8f10b34ae 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -126,6 +126,8 @@ TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line +TGTS ?= + ########## End of parameters ################################################## # What follows may be relevant to you only if you need to # extend this Makefile. If so, look for 'Extension point' here and @@ -237,6 +239,11 @@ vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + VO = vo VOFILES = $(VFILES:.v=.$(VO)) @@ -269,14 +276,14 @@ CMXSFILES = \ PACKEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) # files that are archived into a .cma (mllib) LIBEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) OBJFILES = $(call vo_to_obj,$(VOFILES)) @@ -681,11 +688,11 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ -ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) -else - ifeq ($(MAKECMDGOALS),) +ifndef MAKECMDGOALS -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) endif endif @@ -784,3 +791,7 @@ debug: .PHONY: debug .DEFAULT_GOAL := all + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 226a19678f..4e80caa4cc 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -233,7 +233,7 @@ struct let rem = NSet.fold push next rem in aux rem seen | Some false -> - (** The path we took encountered x -> y but not the one in seen *) + (* The path we took encountered x -> y but not the one in seen *) if through then aux (NMap.add n true rem) (NMap.add n true seen) else aux rem seen | Some true -> aux rem seen @@ -357,7 +357,7 @@ let treat_coq_file chan = | None -> acc | Some file_str -> (canonize file_str, ".v") :: acc else acc - | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *) + | AddLoadPath _ | AddRecLoadPath _ -> acc (* TODO *) in loop acc in diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index db2031c64b..e3dd32fb63 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -132,7 +132,7 @@ let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t) -(** The associated boolean is true if this is a root path. *) +(* The associated boolean is true if this is a root path. *) let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) let get_prefix p l = |