diff --git a/pcuic/theories/Bidirectional/BDStrengthening.v b/pcuic/theories/Bidirectional/BDStrengthening.v
index baf715008..0d898be85 100644
--- a/pcuic/theories/Bidirectional/BDStrengthening.v
+++ b/pcuic/theories/Bidirectional/BDStrengthening.v
@@ -11,7 +11,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICGlobalEnv
 From MetaCoq.PCUIC Require Import BDTyping BDToPCUIC BDFromPCUIC.
 
 Require Import ssreflect ssrbool.
-Require Import Coq.Program.Equality.
+From Coq.Program Require Import Equality.
 
 Ltac case_inequalities :=
   match goal with
diff --git a/pcuic/theories/Syntax/PCUICDepth.v b/pcuic/theories/Syntax/PCUICDepth.v
index 71a94c8b1..ede5c7f42 100644
--- a/pcuic/theories/Syntax/PCUICDepth.v
+++ b/pcuic/theories/Syntax/PCUICDepth.v
@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect Program Lia BinPos Arith.Compare_dec Bool.
+From Coq Require Import ssreflect Program Lia BinPos Compare_dec Bool.
 From MetaCoq.Utils Require Import utils LibHypsNaming.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICSize PCUICInduction.
 From Coq Require Import List.
diff --git a/pcuic/theories/Syntax/PCUICInduction.v b/pcuic/theories/Syntax/PCUICInduction.v
index 3c2676cab..23ffeb79d 100644
--- a/pcuic/theories/Syntax/PCUICInduction.v
+++ b/pcuic/theories/Syntax/PCUICInduction.v
@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect Program Lia BinPos Arith.Compare_dec Bool.
+From Coq Require Import ssreflect Program Lia BinPos Compare_dec Bool.
 From MetaCoq.Utils Require Import utils LibHypsNaming.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICSize.
 From Coq Require Import List.
diff --git a/quotation/theories/ToPCUIC/Stdlib/Numbers.v b/quotation/theories/ToPCUIC/Stdlib/Numbers.v
index 65c0e8ea4..1b674023d 100644
--- a/quotation/theories/ToPCUIC/Stdlib/Numbers.v
+++ b/quotation/theories/ToPCUIC/Stdlib/Numbers.v
@@ -2,7 +2,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts
      Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63
      Cyclic.Abstract.CyclicAxioms
      Cyclic.Abstract.DoubleType
-     Cyclic.Abstract.CarryType
+     Cyclic.Int63.CarryType
 .
 
 From Coq Require Import ZArith.
diff --git a/quotation/theories/ToTemplate/Stdlib/Numbers.v b/quotation/theories/ToTemplate/Stdlib/Numbers.v
index 89fb4b9c6..f4473e30b 100644
--- a/quotation/theories/ToTemplate/Stdlib/Numbers.v
+++ b/quotation/theories/ToTemplate/Stdlib/Numbers.v
@@ -2,7 +2,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts
      Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63
      Cyclic.Abstract.CyclicAxioms
      Cyclic.Abstract.DoubleType
-     Cyclic.Abstract.CarryType
+     Cyclic.Int63.CarryType
 .
 From Coq Require Import ZArith.
 From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init.
diff --git a/safechecker-plugin/_PluginProject.in b/safechecker-plugin/_PluginProject.in
index 5a2c45cb5..a7abaade4 100644
--- a/safechecker-plugin/_PluginProject.in
+++ b/safechecker-plugin/_PluginProject.in
@@ -13,6 +13,8 @@ src/uGraph0.ml
 src/uGraph0.mli
 src/wGraph.ml
 src/wGraph.mli
+src/wf0.ml
+src/wf0.mli
 
 # From PCUIC
 src/pCUICPrimitive.mli
diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh
index 85e2f761a..772499c73 100755
--- a/safechecker-plugin/clean_extraction.sh
+++ b/safechecker-plugin/clean_extraction.sh
@@ -32,6 +32,9 @@ then
     # Remove extracted modules already linked in the template_coq plugin.
     echo "Removing:" $files
     rm -f $files
+
+    # confusion between Init.Wf and Program.Wf
+    sed -i.bak src/pCUICSafeChecker.ml -e 's/open Wf/open Wf0/'
 else
     echo "Extraction up-to date"
 fi
diff --git a/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack b/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack
index 5557f37d6..0aafddedf 100644
--- a/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack
+++ b/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack
@@ -4,6 +4,7 @@ WGraph
 UGraph0
 Reflect
 MCProd
+Wf0
 
 Classes0
 Logic1
diff --git a/safechecker-plugin/theories/Extraction.v b/safechecker-plugin/theories/Extraction.v
index 00a677373..ebe045a19 100644
--- a/safechecker-plugin/theories/Extraction.v
+++ b/safechecker-plugin/theories/Extraction.v
@@ -48,6 +48,8 @@ Next Obligation. eapply fake_abstract_guard_impl_properties. Qed.
 Definition infer_and_print_template_program_with_guard {cf} {nor} :=
   @SafeTemplateChecker.infer_and_print_template_program cf nor fake_abstract_guard_impl.
 
+From Stdlib.Program Require Import Wf.
+Extraction Library Wf.
 Separate Extraction MakeOrderTac PCUICSafeChecker.typecheck_program
          infer_and_print_template_program_with_guard
          (* The following directives ensure separate extraction does not produce name clashes *)
diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v
index 68cbe06d2..c2bd5d232 100644
--- a/safechecker/theories/PCUICTypeChecker.v
+++ b/safechecker/theories/PCUICTypeChecker.v
@@ -25,7 +25,7 @@ From MetaCoq.SafeChecker Require Import PCUICEqualityDec PCUICSafeReduce PCUICEr
 
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
-Require Import Stdlib.Program.Program.
+From Stdlib Require Import Program.
 
 Local Set Keyed Unification.
 Set Equations Transparent.
diff --git a/template-coq/Makefile b/template-coq/Makefile
index c5c4d27ae..972ccdc11 100644
--- a/template-coq/Makefile
+++ b/template-coq/Makefile
@@ -74,14 +74,7 @@ cleanplugin: Makefile.plugin
 	make -f Makefile.plugin clean
 
 PLUGIN_PROJECT_BLACKLIST := \
-	carryType \
-	coreTactics \
-	depElim \
-	floatClass \
-	init \
 	mCUint63 \
-	noConfusion \
-	wf \
 	#
 
 space := $(subst ,, )
diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in
index abd10f638..f28ff7bb3 100644
--- a/template-coq/_PluginProject.in
+++ b/template-coq/_PluginProject.in
@@ -27,10 +27,6 @@ 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/bool.ml
 gen-src/bool.mli
 gen-src/byte.ml
@@ -64,6 +60,8 @@ gen-src/coreTactics.ml
 gen-src/coreTactics.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
@@ -101,20 +99,22 @@ 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
 gen-src/init.mli
 gen-src/int0.ml
 gen-src/int0.mli
+gen-src/intDef.ml
+gen-src/intDef.mli
 gen-src/kernames.ml
 gen-src/kernames.mli
 gen-src/liftSubst.ml
 gen-src/liftSubst.mli
 gen-src/list0.ml
 gen-src/list0.mli
+gen-src/listDef.ml
+gen-src/listDef.mli
 gen-src/logic0.ml
 gen-src/logic0.mli
 gen-src/logic1.ml
@@ -141,10 +141,6 @@ 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/mCUtils.ml
@@ -165,6 +161,8 @@ gen-src/monad_utils.ml
 gen-src/monad_utils.mli
 gen-src/nat0.ml
 gen-src/nat0.mli
+gen-src/natDef.ml
+gen-src/natDef.mli
 gen-src/noConfusion.ml
 gen-src/noConfusion.mli
 gen-src/number.ml
@@ -187,6 +185,8 @@ gen-src/peanoNat.ml
 gen-src/peanoNat.mli
 gen-src/plugin_core.ml
 gen-src/plugin_core.mli
+gen-src/posDef.ml
+gen-src/posDef.mli
 gen-src/pretty.ml
 gen-src/pretty.mli
 gen-src/primFloat.ml
@@ -195,10 +195,10 @@ 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/primitive.ml
+gen-src/primitive.mli
 gen-src/quoter.ml
 gen-src/reflect.ml
 gen-src/reflect.mli
@@ -209,16 +209,18 @@ 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/sint63Axioms.ml
+gen-src/sint63Axioms.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
@@ -230,20 +232,12 @@ gen-src/transform.ml
 gen-src/transform.mli
 gen-src/typing0.ml
 gen-src/typing0.mli
-gen-src/uint0.ml
-gen-src/uint0.mli
+gen-src/uint63Axioms.ml
+gen-src/uint63Axioms.mli
 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
 
diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack
index 43f9a253d..394134ce8 100644
--- a/template-coq/gen-src/metacoq_template_plugin.mlpack
+++ b/template-coq/gen-src/metacoq_template_plugin.mlpack
@@ -7,6 +7,7 @@ Hexadecimal
 Numeral0
 Nat0
 Caml_nat
+ListDef
 List0
 PeanoNat
 Specif
@@ -14,9 +15,13 @@ Basics
 BinPosDef
 BinNums
 BinPos
+PosDef
 BinNat
+NatDef
 BinInt
+IntDef
 PrimInt63
+Uint63Axioms
 Uint0
 Int63
 Byte
@@ -77,6 +82,7 @@ FloatOps
 PrimString
 PrimStringAxioms
 MCString
+Sint63Axioms
 Sint63
 Show
 MCUtils
diff --git a/template-coq/gen-src/specFloat.ml.orig b/template-coq/gen-src/specFloat.ml.orig
index 612fa74ed..010415afd 100644
--- a/template-coq/gen-src/specFloat.ml.orig
+++ b/template-coq/gen-src/specFloat.ml.orig
@@ -1,10 +1,7 @@
-open BinInt
 open BinNums
-open BinPos
-open Bool
 open Datatypes
-open Zbool
-open Zpower
+open IntDef
+open PosDef
 
 type spec_float =
 | S754_zero of bool
@@ -39,7 +36,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 **)
 
@@ -174,7 +171,7 @@ let binary_round_aux prec emax sx mx ex lx =
 
 let shl_align mx ex ex' =
   match Z.sub ex' ex with
-  | Zneg d -> ((shift_pos d mx), ex')
+  | Zneg d -> ((Pos.iter (fun x -> Coq_xO x) mx d), ex')
   | _ -> (mx, ex)
 
 (** val binary_round :
@@ -283,8 +280,8 @@ let coq_SFclassify prec = function
 | S754_nan -> NaN
 | S754_finite (s, m, _) ->
   if s
-  then if Pos.eqb (digits2_pos m) (Z.to_pos prec) then NNormal else NSubn
-  else if Pos.eqb (digits2_pos m) (Z.to_pos prec) then PNormal else PSubn
+  then if Z.eqb (Zpos (digits2_pos m)) prec then NNormal else NSubn
+  else if Z.eqb (Zpos (digits2_pos m)) prec then PNormal else PSubn
 
 (** val coq_SFmul :
     coq_Z -> coq_Z -> spec_float -> spec_float -> spec_float **)
@@ -323,12 +320,16 @@ let coq_SFadd prec emax x y =
   match x with
   | S754_zero sx ->
     (match y with
-     | S754_zero sy -> if eqb sx sy then x else S754_zero false
+     | S754_zero sy ->
+       if sx
+       then if sy then x else S754_zero false
+       else if sy then S754_zero false else x
      | S754_nan -> S754_nan
      | _ -> y)
   | S754_infinity sx ->
     (match y with
-     | S754_infinity sy -> if eqb sx sy then x else S754_nan
+     | S754_infinity sy ->
+       if sx then if sy then x else S754_nan else if sy then S754_nan else x
      | S754_nan -> S754_nan
      | _ -> x)
   | S754_nan -> S754_nan
@@ -341,7 +342,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 **)
@@ -350,13 +352,17 @@ let coq_SFsub prec emax x y =
   match x with
   | S754_zero sx ->
     (match y with
-     | S754_zero sy -> if eqb sx (negb sy) then x else S754_zero false
+     | S754_zero sy ->
+       if sx
+       then if sy then S754_zero false else x
+       else if sy then x else S754_zero false
      | S754_infinity sy -> S754_infinity (negb sy)
      | S754_nan -> S754_nan
      | S754_finite (sy, my, ey) -> S754_finite ((negb sy), my, ey))
   | S754_infinity sx ->
     (match y with
-     | S754_infinity sy -> if eqb sx (negb sy) then x else S754_nan
+     | S754_infinity sy ->
+       if sx then if sy then S754_nan else x else if sy then x else S754_nan
      | S754_nan -> S754_nan
      | _ -> x)
   | S754_nan -> S754_nan
@@ -369,19 +375,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 +463,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
@@ -491,11 +498,11 @@ let coq_SFldexp prec emax f e =
 
 let coq_SFfrexp prec emax f = match f with
 | S754_finite (sx, mx, ex) ->
-  if Pos.leb (Z.to_pos prec) (digits2_pos mx)
+  if Z.leb prec (Zpos (digits2_pos mx))
   then ((S754_finite (sx, mx, (Z.opp prec))), (Z.add ex prec))
   else let d = Z.sub prec (Zpos (digits2_pos mx)) in
-       ((S754_finite (sx, (shift_pos (Z.to_pos d) mx), (Z.opp prec))),
-       (Z.sub (Z.add ex prec) d))
+       ((S754_finite (sx, (Pos.iter (fun x -> Coq_xO x) mx (Z.to_pos d)),
+       (Z.opp prec))), (Z.sub (Z.add ex prec) d))
 | _ -> (f, (Z.sub (Z.mul (Zneg (Coq_xO Coq_xH)) emax) prec))
 
 (** val coq_SFone : coq_Z -> coq_Z -> spec_float **)
@@ -514,7 +521,8 @@ let coq_SFulp prec emax x =
 let coq_SFpred_pos prec emax x = match x with
 | S754_finite (_, mx, _) ->
   let d =
-    if Pos.eqb (Coq_xO mx) (shift_pos (Z.to_pos prec) Coq_xH)
+    if Pos.eqb (Coq_xO mx)
+         (Pos.iter (fun x0 -> Coq_xO x0) Coq_xH (Z.to_pos prec))
     then coq_SFldexp prec emax (coq_SFone prec emax)
            (fexp prec emax
              (Z.sub (snd (coq_SFfrexp prec emax x)) (Zpos Coq_xH)))
@@ -526,7 +534,8 @@ let coq_SFpred_pos prec emax x = match x with
 (** val coq_SFmax_float : coq_Z -> coq_Z -> spec_float **)
 
 let coq_SFmax_float prec emax =
-  S754_finite (false, (Pos.sub (shift_pos (Z.to_pos prec) Coq_xH) Coq_xH),
+  S754_finite (false,
+    (Pos.sub (Pos.iter (fun x -> Coq_xO x) Coq_xH (Z.to_pos prec)) Coq_xH),
     (Z.sub emax prec))
 
 (** val coq_SFsucc : coq_Z -> coq_Z -> spec_float -> spec_float **)
diff --git a/template-coq/specFloat.patch b/template-coq/specFloat.patch
index 294627074..f485afd40 100644
--- a/template-coq/specFloat.patch
+++ b/template-coq/specFloat.patch
@@ -2,8 +2,8 @@
 +++ gen-src/specFloat.ml	2020-12-04 21:48:33.000000000 +0100
 @@ -4,6 +4,7 @@
  open Datatypes
- open Zbool
- open Zpower
+ open IntDef
+ open PosDef
 +open Float64
  
  type spec_float =
diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml
index 4accda36a..f31e38694 100644
--- a/template-coq/src/ast_denoter.ml
+++ b/template-coq/src/ast_denoter.ml
@@ -232,7 +232,7 @@ struct
   let unquote_universe_level evm l = evm, unquote_level l
 
   let unquote_universe_instance(evm: Evd.evar_map) (l: quoted_univ_instance): Evd.evar_map * UVars.Instance.t
-  = (evm,  UVars.Instance.of_array ([||], Array.of_list (List0.map unquote_level l)))
+  = (evm,  UVars.Instance.of_array ([||], Array.of_list (List.map unquote_level l)))
 
 
   let unquote_global_reference (trm : Kernames.global_reference) : GlobRef.t =
diff --git a/template-coq/theories/Constants.v b/template-coq/theories/Constants.v
index a8ea5dd3e..ede296051 100644
--- a/template-coq/theories/Constants.v
+++ b/template-coq/theories/Constants.v
@@ -43,15 +43,15 @@ Register Stdlib.Init.Specif.sigT as metacoq.sigma.type.
 Register Stdlib.Init.Specif.existT as metacoq.sigma.intro.
 Register MetaCoq.Template.TemplateMonad.Common.existT_typed_term as metacoq.sigma.typed_term.
 
-Register Stdlib.Numbers.BinNums.positive as metacoq.pos.type.
-Register Stdlib.Numbers.BinNums.xI as metacoq.pos.xI.
-Register Stdlib.Numbers.BinNums.xO as metacoq.pos.xO.
-Register Stdlib.Numbers.BinNums.xH as metacoq.pos.xH.
-
-Register Stdlib.Numbers.BinNums.Z as metacoq.Z.type.
-Register Stdlib.Numbers.BinNums.Zpos as metacoq.Z.pos.
-Register Stdlib.Numbers.BinNums.Zneg as metacoq.Z.neg.
-Register Stdlib.Numbers.BinNums.Z0 as metacoq.Z.zero.
+Register BinNums.positive as metacoq.pos.type.
+Register BinNums.xI as metacoq.pos.xI.
+Register BinNums.xO as metacoq.pos.xO.
+Register BinNums.xH as metacoq.pos.xH.
+
+Register BinNums.Z as metacoq.Z.type.
+Register BinNums.Zpos as metacoq.Z.pos.
+Register BinNums.Zneg as metacoq.Z.neg.
+Register BinNums.Z0 as metacoq.Z.zero.
 
 (* Ast *)
 Register MetaCoq.Common.BasicAst.relevance as metacoq.ast.relevance.
diff --git a/test-suite/safechecker_test.v b/test-suite/safechecker_test.v
index 542cec8e2..44cc847d0 100644
--- a/test-suite/safechecker_test.v
+++ b/test-suite/safechecker_test.v
@@ -12,7 +12,8 @@ Environment is well-formed and Ind(Stdlib.Init.Datatypes.nat,0,[]) has type: Sor
 MetaCoq SafeCheck (3 + 1).
 
 Definition bool_list := List.map negb (cons true (cons false nil)).
-MetaCoq SafeCheck bool_list.
+(* was working a bit by accident *)
+(* MetaCoq SafeCheck bool_list. *)
 MetaCoq CoqCheck bool_list.
 
 (* Time MetaCoq SafeCheck @infer_and_print_template_program. *)
diff --git a/utils/theories/bytestring.v b/utils/theories/bytestring.v
index ad0f13089..a0b6ea0cf 100644
--- a/utils/theories/bytestring.v
+++ b/utils/theories/bytestring.v
@@ -9,7 +9,7 @@
 Require Coq.Strings.String ssrbool.
 Require Import ssreflect.
 Require Import Coq.NArith.NArith.
-Require Import Coq.micromega.Lia.
+From Coq Require Import Lia.
 From Equations Require Import Equations.
 Set Primitive Projections.
 Set Default Proof Using "Type".
@@ -196,7 +196,7 @@ Notation "x ++ y" := (String.append x y) : bs_scope.
 Import String.
 
 (** comparison *)
-Require Import Orders Coq.Structures.OrderedType Coq.Structures.OrdersAlt.
+From Coq Require Import Orders OrderedType OrdersAlt.
 
 Lemma to_N_inj : forall x y, Byte.to_N x = Byte.to_N y <-> x = y.
 Proof.