From 34f146d10e0c50f029fdb49f2b229761025fcac3 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Sun, 3 Nov 2024 20:39:57 +0000
Subject: [PATCH] adapt to Zeq_bool:=Z.eqb
 (https://github.com/coq/coq/pull/19801)

---
 template-coq/_PluginProject.in | 60 +++++++++++++++++-----------------
 template-pcuic/metacoq-config  |  2 +-
 2 files changed, 31 insertions(+), 31 deletions(-)

diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in
index f28ff7bb3..0dda94e3d 100644
--- a/template-coq/_PluginProject.in
+++ b/template-coq/_PluginProject.in
@@ -4,6 +4,10 @@
 META.coq-metacoq-template-ocaml
 -I .
 
+gen-src/metacoq_template_plugin.mlpack
+
+theories/ExtractableLoader.v
+
 # Generated Code by `ls -1 gen-src/*.ml gen-src/*.mli` in `template-coq/` after having compiled `Extraction.v`
 gen-src/all_Forall.ml
 gen-src/all_Forall.mli
@@ -11,10 +15,10 @@ gen-src/ascii.ml
 gen-src/ascii.mli
 gen-src/ast0.ml
 gen-src/ast0.mli
-gen-src/astUtils.ml
-gen-src/astUtils.mli
 gen-src/ast_denoter.ml
 gen-src/ast_quoter.ml
+gen-src/astUtils.ml
+gen-src/astUtils.mli
 gen-src/basicAst.ml
 gen-src/basicAst.mli
 gen-src/basics.ml
@@ -29,18 +33,16 @@ gen-src/binPos.ml
 gen-src/binPos.mli
 gen-src/bool.ml
 gen-src/bool.mli
-gen-src/byte.ml
-gen-src/byte.mli
 gen-src/byte0.ml
 gen-src/byte0.mli
 gen-src/byteCompare.ml
 gen-src/byteCompare.mli
 gen-src/byteCompareSpec.ml
 gen-src/byteCompareSpec.mli
+gen-src/byte.ml
+gen-src/byte.mli
 gen-src/bytestring.ml
 gen-src/bytestring.mli
-gen-src/cRelationClasses.ml
-gen-src/cRelationClasses.mli
 gen-src/caml_byte.ml
 gen-src/caml_byte.mli
 gen-src/caml_bytestring.ml
@@ -58,6 +60,8 @@ gen-src/config0.ml
 gen-src/config0.mli
 gen-src/coreTactics.ml
 gen-src/coreTactics.mli
+gen-src/cRelationClasses.ml
+gen-src/cRelationClasses.mli
 gen-src/datatypes.ml
 gen-src/datatypes.mli
 gen-src/decidableClass.ml
@@ -69,22 +73,26 @@ gen-src/decimal.mli
 gen-src/denoter.ml
 gen-src/depElim.ml
 gen-src/depElim.mli
-gen-src/envMap.ml
-gen-src/envMap.mli
 gen-src/environment.ml
 gen-src/environment.mli
 gen-src/environmentTyping.ml
 gen-src/environmentTyping.mli
-gen-src/eqDec.ml
-gen-src/eqDec.mli
+gen-src/envMap.ml
+gen-src/envMap.mli
 gen-src/eqDecInstances.ml
 gen-src/eqDecInstances.mli
+gen-src/eqDec.ml
+gen-src/eqDec.mli
 gen-src/eqdepFacts.ml
 gen-src/eqdepFacts.mli
 gen-src/equalities.ml
 gen-src/equalities.mli
 gen-src/extractable.ml
 gen-src/extractable.mli
+gen-src/floatClass.ml
+gen-src/floatClass.mli
+gen-src/floatOps.ml
+gen-src/floatOps.mli
 gen-src/fMapAVL.ml
 gen-src/fMapAVL.mli
 gen-src/fMapFacts.ml
@@ -93,10 +101,6 @@ gen-src/fMapInterface.ml
 gen-src/fMapInterface.mli
 gen-src/fMapList.ml
 gen-src/fMapList.mli
-gen-src/floatClass.ml
-gen-src/floatClass.mli
-gen-src/floatOps.ml
-gen-src/floatOps.mli
 gen-src/hexadecimal.ml
 gen-src/hexadecimal.mli
 gen-src/induction0.ml
@@ -141,10 +145,12 @@ gen-src/mCRelations.ml
 gen-src/mCRelations.mli
 gen-src/mCString.ml
 gen-src/mCString.mli
-# gen-src/mCUint63.ml
-# gen-src/mCUint63.mli
+#gen-src/mCUint63.ml
+#gen-src/mCUint63.mli
 gen-src/mCUtils.ml
 gen-src/mCUtils.mli
+gen-src/monad_utils.ml
+gen-src/monad_utils.mli
 gen-src/mSetAVL.ml
 gen-src/mSetAVL.mli
 gen-src/mSetDecide.ml
@@ -157,8 +163,6 @@ gen-src/mSetList.ml
 gen-src/mSetList.mli
 gen-src/mSetProperties.ml
 gen-src/mSetProperties.mli
-gen-src/monad_utils.ml
-gen-src/monad_utils.mli
 gen-src/nat0.ml
 gen-src/nat0.mli
 gen-src/natDef.ml
@@ -171,14 +175,14 @@ gen-src/orderedType0.ml
 gen-src/orderedType0.mli
 gen-src/orderedTypeAlt.ml
 gen-src/orderedTypeAlt.mli
-gen-src/orders.ml
-gen-src/orders.mli
 gen-src/ordersAlt.ml
 gen-src/ordersAlt.mli
 gen-src/ordersFacts.ml
 gen-src/ordersFacts.mli
 gen-src/ordersLists.ml
 gen-src/ordersLists.mli
+gen-src/orders.ml
+gen-src/orders.mli
 gen-src/ordersTac.ml
 gen-src/ordersTac.mli
 gen-src/peanoNat.ml
@@ -193,17 +197,17 @@ gen-src/primFloat.ml
 gen-src/primFloat.mli
 gen-src/primInt63.ml
 gen-src/primInt63.mli
-gen-src/primString.ml
-gen-src/primString.mli
-gen-src/primStringAxioms.ml
-gen-src/primStringAxioms.mli
 gen-src/primitive.ml
 gen-src/primitive.mli
+gen-src/primStringAxioms.ml
+gen-src/primStringAxioms.mli
+gen-src/primString.ml
+gen-src/primString.mli
 gen-src/quoter.ml
-gen-src/reflect.ml
-gen-src/reflect.mli
 gen-src/reflectEq.ml
 gen-src/reflectEq.mli
+gen-src/reflect.ml
+gen-src/reflect.mli
 gen-src/reification.ml
 gen-src/relation.ml
 gen-src/relation.mli
@@ -238,7 +242,3 @@ gen-src/universes0.ml
 gen-src/universes0.mli
 gen-src/wf.ml
 gen-src/wf.mli
-
-gen-src/metacoq_template_plugin.mlpack
-
-theories/ExtractableLoader.v
diff --git a/template-pcuic/metacoq-config b/template-pcuic/metacoq-config
index 7fe94ce25..00bfe61cd 100644
--- a/template-pcuic/metacoq-config
+++ b/template-pcuic/metacoq-config
@@ -1,2 +1,2 @@
 # DO NOT EDIT THIS FILE: autogenerated from ./configure.sh
-
+-R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common -R ../pcuic/theories MetaCoq.PCUIC -R ../template-coq/theories MetaCoq.Template -I ../template-coq