adapt to Zeq_bool:=Z.eqb (coq/coq#19801)

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
@@ -25,26 +29,22 @@ gen-src/binNat.ml
 gen-src/binNat.mli
 gen-src/binNums.ml
 gen-src/binNums.mli
-gen-src/binPos.ml
-gen-src/binPos.mli
 gen-src/binPosDef.ml
 gen-src/binPosDef.mli
-gen-src/decidableClass.mli
-gen-src/decidableClass.ml
+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
@@ -62,31 +62,39 @@ 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
+gen-src/decidableClass.mli
 gen-src/decidableType.ml
 gen-src/decidableType.mli
 gen-src/decimal.ml
 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
@@ -95,14 +103,8 @@ 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/hexadecimalString.ml
-# gen-src/hexadecimalString.mli
 gen-src/induction0.ml
 gen-src/induction0.mli
 gen-src/init.ml
@@ -141,14 +143,12 @@ gen-src/mCRelations.ml
 gen-src/mCRelations.mli
 gen-src/mCString.ml
 gen-src/mCString.mli
-gen-src/sint63.mli
-gen-src/sint63.ml
-gen-src/show.mli
-gen-src/show.ml
-# 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
@@ -161,8 +161,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/noConfusion.ml
@@ -173,14 +171,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,32 +191,34 @@ 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/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
 gen-src/run_extractable.ml
 gen-src/run_extractable.mli
+gen-src/show.ml
+gen-src/show.mli
 gen-src/signature.ml
 gen-src/signature.mli
+gen-src/sint63.ml
+gen-src/sint63.mli
 gen-src/specFloat.ml
 gen-src/specFloat.mli
 gen-src/specif.ml
 gen-src/specif.mli
 gen-src/string0.ml
 gen-src/string0.mli
-gen-src/sumbool.ml
-gen-src/sumbool.mli
 gen-src/templateEnvMap.ml
 gen-src/templateEnvMap.mli
 gen-src/templateProgram.ml
@@ -236,15 +236,5 @@ gen-src/universes0.ml
 gen-src/universes0.mli
 gen-src/wf.ml
 gen-src/wf.mli
-gen-src/zArith_dec.ml
-gen-src/zArith_dec.mli
-gen-src/zbool.ml
-gen-src/zbool.mli
-gen-src/zeven.ml
-gen-src/zeven.mli
 gen-src/zpower.ml
 gen-src/zpower.mli
-
-gen-src/metacoq_template_plugin.mlpack
-
-theories/ExtractableLoader.v

template-coq/gen-src/specFloat.ml.orig

@@ -3,7 +3,6 @@ open BinNums
 open BinPos
 open Bool
 open Datatypes
-open Zbool
 open Zpower
 
 type spec_float =
@@ -39,7 +38,7 @@ let coq_Zdigits2 n = match n with
 (** val canonical_mantissa : coq_Z -> coq_Z -> positive -> coq_Z -> bool **)
 
 let canonical_mantissa prec emax m e =
-  coq_Zeq_bool (fexp prec emax (Z.add (Zpos (digits2_pos m)) e)) e
+  Z.eqb (fexp prec emax (Z.add (Zpos (digits2_pos m)) e)) e
 
 (** val bounded : coq_Z -> coq_Z -> positive -> coq_Z -> bool **)
 
@@ -341,7 +340,8 @@ let coq_SFadd prec emax x y =
        let ez = Z.min ex ey in
        binary_normalize prec emax
          (Z.add (cond_Zopp sx (Zpos (fst (shl_align mx ex ez))))
-           (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) ez false)
+           (cond_Zopp sy (Zpos (fst (shl_align my ey ez)))))
+         ez false)
 
 (** val coq_SFsub :
     coq_Z -> coq_Z -> spec_float -> spec_float -> spec_float **)
@@ -369,19 +369,20 @@ let coq_SFsub prec emax x y =
        let ez = Z.min ex ey in
        binary_normalize prec emax
          (Z.sub (cond_Zopp sx (Zpos (fst (shl_align mx ex ez))))
-           (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) ez false)
+           (cond_Zopp sy (Zpos (fst (shl_align my ey ez)))))
+         ez false)
 
 (** val new_location_even : coq_Z -> coq_Z -> location **)
 
 let new_location_even nb_steps k =
-  if coq_Zeq_bool k Z0
+  if Z.eqb k Z0
   then Coq_loc_Exact
   else Coq_loc_Inexact (Z.compare (Z.mul (Zpos (Coq_xO Coq_xH)) k) nb_steps)
 
 (** val new_location_odd : coq_Z -> coq_Z -> location **)
 
 let new_location_odd nb_steps k =
-  if coq_Zeq_bool k Z0
+  if Z.eqb k Z0
   then Coq_loc_Exact
   else Coq_loc_Inexact
          (match Z.compare
@@ -456,7 +457,7 @@ let coq_SFsqrt_core_binary prec emax m e =
            | Zneg _ -> Z0 in
   let (q, r) = Z.sqrtrem m' in
   let l =
-    if coq_Zeq_bool r Z0
+    if Z.eqb r Z0
     then Coq_loc_Exact
     else Coq_loc_Inexact (if Z.leb r q then Lt else Gt)
   in