diff --git a/Makefile b/Makefile index 8a6cd1f98..e47d35a52 100644 --- a/Makefile +++ b/Makefile @@ -114,6 +114,11 @@ ML_COMPATIBILITY_FILES_PATTERN := src/Common/Tactics/hint_db_extra_tactics.ml sr ML_COMPATIBILITY_FILES := $(subst @ML4_OR_MLG@,$(ML4_OR_MLG),$(ML_COMPATIBILITY_FILES_PATTERN)) +MAKEFILE_COQ_COMMON_CONTENTS := $(shell grep -- '-include Makefile.coq' etc/coq-scripts/Makefile.coq.common) +ifneq ($(MAKEFILE_COQ_COMMON_CONTENTS),) +$(error "Your coq-scripts submodule is too old! Please update it. Hopefully this error message will prevent future silent failures on Coq's CI as fixed twice now, e.g., by 75a2142c94a90a45287389d26a26ea5322e84f7e") +endif + include etc/coq-scripts/Makefile.coq.common include etc/coq-scripts/compatibility/Makefile.coq.compat_84_85 @@ -314,7 +319,7 @@ install-fiat install-fiat-core install-querystructures install-parsers install-p # This target is used to update the _CoqProject.in file. # Use -R, not -I for Bedrock, as it is Coq input, not OCaml input. $(UPDATE_COQPROJECT_TARGET): - (echo '-R src Fiat'; echo '-R Bedrock Bedrock'; echo '-I src/Common/Tactics'; git ls-files "*.v" | grep -v '^$(COMPATIBILITY_FILE)$$' | $(SORT_COQPROJECT); (echo '$(COMPATIBILITY_FILE)'; git ls-files "*.{ml4,mlg}" | $(SORT_COQPROJECT); (echo '$(ML_COMPATIBILITY_FILES)' | tr ' ' '\n'; echo 'src/Common/Tactics/transparent_abstract_plugin.mllib'; echo 'src/Common/Tactics/hint_db_extra_plugin.mllib') | $(SORT_COQPROJECT))) > _CoqProject.in + (echo '-R src Fiat'; echo '-R Bedrock Bedrock'; echo '-I src/Common/Tactics'; git ls-files "*.v" | grep -v '^$(COMPATIBILITY_FILE)$$' | $(SORT_COQPROJECT); (echo '$(COMPATIBILITY_FILE)'; git ls-files "*.{ml4,mlg}" | $(SORT_COQPROJECT); (echo '$(ML_COMPATIBILITY_FILES_PATTERN)' | tr ' ' '\n'; echo 'src/Common/Tactics/transparent_abstract_plugin.mllib'; echo 'src/Common/Tactics/hint_db_extra_plugin.mllib') | $(SORT_COQPROJECT))) > _CoqProject.in ifeq ($(IS_FAST),0) # see http://stackoverflow.com/a/9691619/377022 for why we need $(eval $(call ...)) diff --git a/_CoqProject.in b/_CoqProject.in index 021f42a5a..88f7d1d52 100644 --- a/_CoqProject.in +++ b/_CoqProject.in @@ -312,9 +312,9 @@ src/QueryStructure/Specification/SearchTerms/InRange.v src/QueryStructure/Specification/SearchTerms/ListInclusion.v src/QueryStructure/Specification/SearchTerms/ListPrefix.v src/Common/Coq__8_4__8_5__Compat.v -src/Common/Tactics/hint_db_extra_plugin.ml4 +src/Common/Tactics/hint_db_extra_plugin.@ML4_OR_MLG@ src/Common/Tactics/hint_db_extra_plugin.mllib src/Common/Tactics/hint_db_extra_tactics.ml -src/Common/Tactics/transparent_abstract_plugin.ml4 +src/Common/Tactics/transparent_abstract_plugin.@ML4_OR_MLG@ src/Common/Tactics/transparent_abstract_plugin.mllib src/Common/Tactics/transparent_abstract_tactics.ml diff --git a/etc/coq-scripts b/etc/coq-scripts index 7bd683da1..9dc70c73b 160000 --- a/etc/coq-scripts +++ b/etc/coq-scripts @@ -1 +1 @@ -Subproject commit 7bd683da1fac8b5eb42de1e44a3274db4fd0ce41 +Subproject commit 9dc70c73be0d6a35c09136d65b5f21b75b77d273