Adapt to https://github.com/rocq-prover/rocq/pull/21955

.gitignore

@@ -100,6 +100,7 @@ src/Rewriter/Util/plugins/RewriterBuildRegistry.v
 src/Rewriter/Util/plugins/RewriterBuild.v
 src/Rewriter/Util/plugins/StrategyTactic.v
 src/Rewriter/Util/plugins/Ltac2Extra.v
+src/Rewriter/Util/plugins/META.coq-rewriter
 src/Rewriter/Util/plugins/definition_by_tactic.ml
 src/Rewriter/Util/plugins/definition_by_tactic.mli
 src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg

Makefile

@@ -49,7 +49,7 @@ endif
 endif
 
 _CoqProject: _CoqProject.in
-	sed 's?@META@?$(META_FILE_FRAGMENT)?g' $< > $@
+	cp $< $@
 
 # This target is used to update the _CoqProject file.
 # But it only works if we have git
@@ -58,7 +58,7 @@ SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
 EXISTING_COQPROJECT_CONTENTS_SORTED:=$(shell cat _CoqProject.in 2>&1 | $(SORT_COQPROJECT))
 WARNINGS_PLUS := +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field
 WARNINGS := $(WARNINGS_PLUS),unsupported-attributes
-COQPROJECT_CMD:=(echo @META@; echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-I $(PLUGINS_DIR)'; echo '-arg -w -arg $(WARNINGS)'; echo '-arg -native-compiler -arg ondemand'; (git ls-files '$(SRC_DIR)/*.v' '$(SRC_DIR)/*.mlg' '$(SRC_DIR)/*.mllib' '$(SRC_DIR)/*.ml' '$(SRC_DIR)/*.mli' | $(SORT_COQPROJECT)); (echo '$(COMPATIBILITY_FILES)' | tr ' ' '\n'))
+COQPROJECT_CMD:=(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-I $(PLUGINS_DIR)'; echo '-arg -w -arg $(WARNINGS)'; echo '-arg -native-compiler -arg ondemand'; (git ls-files '$(SRC_DIR)/*.v' '$(SRC_DIR)/*.mlg' '$(SRC_DIR)/*.mllib' '$(SRC_DIR)/*.ml' '$(SRC_DIR)/*.mli' | $(SORT_COQPROJECT)); (echo '$(COMPATIBILITY_FILES)' | tr ' ' '\n'))
 NEW_COQPROJECT_CONTENTS_SORTED:=$(shell $(COQPROJECT_CMD) | $(SORT_COQPROJECT))
 
 ifneq ($(EXISTING_COQPROJECT_CONTENTS_SORTED),$(NEW_COQPROJECT_CONTENTS_SORTED))

Makefile.local-late

@@ -17,4 +17,8 @@ OTHERFLAGS += -profile-ltac
 endif
 
 # Kludge around COQBUG(https://github.com/coq/coq/issues/16591)
+ifneq (,$(filter .v815 .v816 .v817 .v818 .v819 .v820 .v821 .v90 .v91 .v92,$(EXPECTED_EXT)))
 FINDLIBPKGS += -package coq-core.plugins.ltac2
+else
+FINDLIBPKGS += -package rocq-runtime.plugins.ltac2
+endif

Makefile.local.common

@@ -31,9 +31,7 @@ COQ_EXTENDED_VERSION_OLD:=$(strip $(shell cat $(COQ_VERSION_FILE) 2>/dev/null))
 ifneq (,$(filter 8.15%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v815
 ML_DESCRIPTION := "Coq v8.15"
-META_FILE_FRAGMENT :=
 else
-META_FILE_FRAGMENT := src/Rewriter/Util/plugins/META.coq-rewriter
 ifneq (,$(filter 8.16%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v816
 ML_DESCRIPTION := "Coq v8.16"
@@ -84,6 +82,7 @@ endif
 endif
 
 COMPATIBILITY_FILES := \
+	src/Rewriter/Util/plugins/META.coq-rewriter \
 	src/Rewriter/Util/plugins/definition_by_tactic.ml \
 	src/Rewriter/Util/plugins/definition_by_tactic.mli \
 	src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg \

_CoqProject.in

@@ -1,4 +1,3 @@
-@META@
 -R src/Rewriter Rewriter
 -I src/Rewriter/Util/plugins
 -arg -w -arg +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field,unsupported-attributes
@@ -146,6 +145,7 @@ src/Rewriter/Util/Tactics2/ReplaceByPattern.v
 src/Rewriter/Util/Tactics2/String.v
 src/Rewriter/Util/Tactics2/Constr/Unsafe/MakeAbbreviations.v
 src/Rewriter/Util/plugins/RewriterBuildRegistryImports.v
+src/Rewriter/Util/plugins/META.coq-rewriter
 src/Rewriter/Util/plugins/definition_by_tactic.ml
 src/Rewriter/Util/plugins/definition_by_tactic.mli
 src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg

src/Rewriter/Util/plugins/META.coq-rewriter.v817

@@ -0,0 +1,46 @@
+package "strategy_tactic" (
+  directory = "."
+  description = "Coq Strategy Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "strategy_tactic_plugin.cma"
+  archive(native) = "strategy_tactic_plugin.cmxa"
+  plugin(byte) = "strategy_tactic_plugin.cma"
+  plugin(native) = "strategy_tactic_plugin.cmxs"
+)
+package "definition_by_tactic" (
+  directory = "."
+  description = "Coq Definition By Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "definition_by_tactic_plugin.cma"
+  archive(native) = "definition_by_tactic_plugin.cmxa"
+  plugin(byte) = "definition_by_tactic_plugin.cma"
+  plugin(native) = "definition_by_tactic_plugin.cmxs"
+)
+package "inductive_from_elim" (
+  directory = "."
+  description = "Coq Inductive From Elim"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "inductive_from_elim_plugin.cma"
+  archive(native) = "inductive_from_elim_plugin.cmxa"
+  plugin(byte) = "inductive_from_elim_plugin.cma"
+  plugin(native) = "inductive_from_elim_plugin.cmxs"
+)
+package "rewriter_build" (
+  directory = "."
+  description = "Coq Rewriter Build"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "rewriter_build_plugin.cma"
+  archive(native) = "rewriter_build_plugin.cmxa"
+  plugin(byte) = "rewriter_build_plugin.cma"
+  plugin(native) = "rewriter_build_plugin.cmxs"
+)
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
+directory = "."

src/Rewriter/Util/plugins/META.coq-rewriter.v818

@@ -0,0 +1,46 @@
+package "strategy_tactic" (
+  directory = "."
+  description = "Coq Strategy Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "strategy_tactic_plugin.cma"
+  archive(native) = "strategy_tactic_plugin.cmxa"
+  plugin(byte) = "strategy_tactic_plugin.cma"
+  plugin(native) = "strategy_tactic_plugin.cmxs"
+)
+package "definition_by_tactic" (
+  directory = "."
+  description = "Coq Definition By Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "definition_by_tactic_plugin.cma"
+  archive(native) = "definition_by_tactic_plugin.cmxa"
+  plugin(byte) = "definition_by_tactic_plugin.cma"
+  plugin(native) = "definition_by_tactic_plugin.cmxs"
+)
+package "inductive_from_elim" (
+  directory = "."
+  description = "Coq Inductive From Elim"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "inductive_from_elim_plugin.cma"
+  archive(native) = "inductive_from_elim_plugin.cmxa"
+  plugin(byte) = "inductive_from_elim_plugin.cma"
+  plugin(native) = "inductive_from_elim_plugin.cmxs"
+)
+package "rewriter_build" (
+  directory = "."
+  description = "Coq Rewriter Build"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "rewriter_build_plugin.cma"
+  archive(native) = "rewriter_build_plugin.cmxa"
+  plugin(byte) = "rewriter_build_plugin.cma"
+  plugin(native) = "rewriter_build_plugin.cmxs"
+)
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
+directory = "."

src/Rewriter/Util/plugins/META.coq-rewriter.v819

@@ -0,0 +1,46 @@
+package "strategy_tactic" (
+  directory = "."
+  description = "Coq Strategy Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "strategy_tactic_plugin.cma"
+  archive(native) = "strategy_tactic_plugin.cmxa"
+  plugin(byte) = "strategy_tactic_plugin.cma"
+  plugin(native) = "strategy_tactic_plugin.cmxs"
+)
+package "definition_by_tactic" (
+  directory = "."
+  description = "Coq Definition By Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "definition_by_tactic_plugin.cma"
+  archive(native) = "definition_by_tactic_plugin.cmxa"
+  plugin(byte) = "definition_by_tactic_plugin.cma"
+  plugin(native) = "definition_by_tactic_plugin.cmxs"
+)
+package "inductive_from_elim" (
+  directory = "."
+  description = "Coq Inductive From Elim"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "inductive_from_elim_plugin.cma"
+  archive(native) = "inductive_from_elim_plugin.cmxa"
+  plugin(byte) = "inductive_from_elim_plugin.cma"
+  plugin(native) = "inductive_from_elim_plugin.cmxs"
+)
+package "rewriter_build" (
+  directory = "."
+  description = "Coq Rewriter Build"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "rewriter_build_plugin.cma"
+  archive(native) = "rewriter_build_plugin.cmxa"
+  plugin(byte) = "rewriter_build_plugin.cma"
+  plugin(native) = "rewriter_build_plugin.cmxs"
+)
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
+directory = "."

src/Rewriter/Util/plugins/META.coq-rewriter.v820

@@ -0,0 +1,46 @@
+package "strategy_tactic" (
+  directory = "."
+  description = "Coq Strategy Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "strategy_tactic_plugin.cma"
+  archive(native) = "strategy_tactic_plugin.cmxa"
+  plugin(byte) = "strategy_tactic_plugin.cma"
+  plugin(native) = "strategy_tactic_plugin.cmxs"
+)
+package "definition_by_tactic" (
+  directory = "."
+  description = "Coq Definition By Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "definition_by_tactic_plugin.cma"
+  archive(native) = "definition_by_tactic_plugin.cmxa"
+  plugin(byte) = "definition_by_tactic_plugin.cma"
+  plugin(native) = "definition_by_tactic_plugin.cmxs"
+)
+package "inductive_from_elim" (
+  directory = "."
+  description = "Coq Inductive From Elim"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "inductive_from_elim_plugin.cma"
+  archive(native) = "inductive_from_elim_plugin.cmxa"
+  plugin(byte) = "inductive_from_elim_plugin.cma"
+  plugin(native) = "inductive_from_elim_plugin.cmxs"
+)
+package "rewriter_build" (
+  directory = "."
+  description = "Coq Rewriter Build"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "rewriter_build_plugin.cma"
+  archive(native) = "rewriter_build_plugin.cmxa"
+  plugin(byte) = "rewriter_build_plugin.cma"
+  plugin(native) = "rewriter_build_plugin.cmxs"
+)
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
+directory = "."

src/Rewriter/Util/plugins/META.coq-rewriter.v821

@@ -0,0 +1,46 @@
+package "strategy_tactic" (
+  directory = "."
+  description = "Coq Strategy Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "strategy_tactic_plugin.cma"
+  archive(native) = "strategy_tactic_plugin.cmxa"
+  plugin(byte) = "strategy_tactic_plugin.cma"
+  plugin(native) = "strategy_tactic_plugin.cmxs"
+)
+package "definition_by_tactic" (
+  directory = "."
+  description = "Coq Definition By Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "definition_by_tactic_plugin.cma"
+  archive(native) = "definition_by_tactic_plugin.cmxa"
+  plugin(byte) = "definition_by_tactic_plugin.cma"
+  plugin(native) = "definition_by_tactic_plugin.cmxs"
+)
+package "inductive_from_elim" (
+  directory = "."
+  description = "Coq Inductive From Elim"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "inductive_from_elim_plugin.cma"
+  archive(native) = "inductive_from_elim_plugin.cmxa"
+  plugin(byte) = "inductive_from_elim_plugin.cma"
+  plugin(native) = "inductive_from_elim_plugin.cmxs"
+)
+package "rewriter_build" (
+  directory = "."
+  description = "Coq Rewriter Build"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "rewriter_build_plugin.cma"
+  archive(native) = "rewriter_build_plugin.cmxa"
+  plugin(byte) = "rewriter_build_plugin.cma"
+  plugin(native) = "rewriter_build_plugin.cmxs"
+)
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
+directory = "."

src/Rewriter/Util/plugins/META.coq-rewriter.v90

@@ -0,0 +1,46 @@
+package "strategy_tactic" (
+  directory = "."
+  description = "Coq Strategy Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "strategy_tactic_plugin.cma"
+  archive(native) = "strategy_tactic_plugin.cmxa"
+  plugin(byte) = "strategy_tactic_plugin.cma"
+  plugin(native) = "strategy_tactic_plugin.cmxs"
+)
+package "definition_by_tactic" (
+  directory = "."
+  description = "Coq Definition By Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "definition_by_tactic_plugin.cma"
+  archive(native) = "definition_by_tactic_plugin.cmxa"
+  plugin(byte) = "definition_by_tactic_plugin.cma"
+  plugin(native) = "definition_by_tactic_plugin.cmxs"
+)
+package "inductive_from_elim" (
+  directory = "."
+  description = "Coq Inductive From Elim"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "inductive_from_elim_plugin.cma"
+  archive(native) = "inductive_from_elim_plugin.cmxa"
+  plugin(byte) = "inductive_from_elim_plugin.cma"
+  plugin(native) = "inductive_from_elim_plugin.cmxs"
+)
+package "rewriter_build" (
+  directory = "."
+  description = "Coq Rewriter Build"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "rewriter_build_plugin.cma"
+  archive(native) = "rewriter_build_plugin.cmxa"
+  plugin(byte) = "rewriter_build_plugin.cma"
+  plugin(native) = "rewriter_build_plugin.cmxs"
+)
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
+directory = "."

src/Rewriter/Util/plugins/META.coq-rewriter.v91

@@ -0,0 +1,46 @@
+package "strategy_tactic" (
+  directory = "."
+  description = "Coq Strategy Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "strategy_tactic_plugin.cma"
+  archive(native) = "strategy_tactic_plugin.cmxa"
+  plugin(byte) = "strategy_tactic_plugin.cma"
+  plugin(native) = "strategy_tactic_plugin.cmxs"
+)
+package "definition_by_tactic" (
+  directory = "."
+  description = "Coq Definition By Tactic"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "definition_by_tactic_plugin.cma"
+  archive(native) = "definition_by_tactic_plugin.cmxa"
+  plugin(byte) = "definition_by_tactic_plugin.cma"
+  plugin(native) = "definition_by_tactic_plugin.cmxs"
+)
+package "inductive_from_elim" (
+  directory = "."
+  description = "Coq Inductive From Elim"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "inductive_from_elim_plugin.cma"
+  archive(native) = "inductive_from_elim_plugin.cmxa"
+  plugin(byte) = "inductive_from_elim_plugin.cma"
+  plugin(native) = "inductive_from_elim_plugin.cmxs"
+)
+package "rewriter_build" (
+  directory = "."
+  description = "Coq Rewriter Build"
+  requires = "coq-core.plugins.ltac"
+  archive(byte) = "rewriter_build_plugin.cma"
+  archive(native) = "rewriter_build_plugin.cmxa"
+  plugin(byte) = "rewriter_build_plugin.cma"
+  plugin(native) = "rewriter_build_plugin.cmxs"
+)
+package "ltac2_extra" (
+  directory = "."
+  description = "Coq Ltac2 Extra Tactics"
+  requires = "coq-core.plugins.ltac2"
+  archive(byte) = "ltac2_extra_plugin.cma"
+  archive(native) = "ltac2_extra_plugin.cmxa"
+  plugin(byte) = "ltac2_extra_plugin.cma"
+  plugin(native) = "ltac2_extra_plugin.cmxs"
+)
+directory = "."