adapt to Zeq_bool:=Z.eqb (rocq-prover/rocq#19801)

Author: andres-erbsen

template-coq/_PluginProject.in

@@ -4,17 +4,21 @@
 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
 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

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