diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index bec6c1b4..9b3975b8 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -19,7 +19,7 @@ jobs:
         opam_file:
           - 'coq-certicoq.opam'
         image:
-          - 'yforster/coq:8.17.0--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3--elpi.1.17.1-metacoq-v1.3-8.17'
+          - 'yforster/coq:8.19.1--clang-11--compcert-3.13.1--extlib-0.12.1--equations-1.3--metacoq-1.3.1'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v3
@@ -51,6 +51,6 @@ jobs:
               make -C ~/repo/benchmarks all
             endGroup
             startGroup "Test bootstrapped plugins"
-              cd repo && ./configure.sh global
+              cd ~/repo && ./configure.sh global
               make -C ~/repo/bootstrap test
             endGroup
diff --git a/.gitignore b/.gitignore
index 63904e4e..82cdec42 100644
--- a/.gitignore
+++ b/.gitignore
@@ -137,3 +137,5 @@ bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
 bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.h
 bootstrap/certicoqc/tests/test.demo1.c
 bootstrap/certicoqc/tests/test.demo1.h
+plugin/.filestoinstall
+cplugin/.merlin
diff --git a/benchmarks/certicoq_eval.v b/benchmarks/certicoq_eval.v
index 00383551..283fa062 100644
--- a/benchmarks/certicoq_eval.v
+++ b/benchmarks/certicoq_eval.v
@@ -1,7 +1,7 @@
 From Equations Require Import Equations.
 From Coq Require Import Uint63 Wf_nat ZArith Lia Arith.
 From CertiCoq Require Import CertiCoq.
-
+CertiCoq -help.
 Set CertiCoq Build Directory "_build".
 
 (* This warns about uses of primitive operations, but we compile them fine *)
@@ -13,8 +13,8 @@ Program Definition long_vector n : Vector.t nat n :=
   Vector.of_list (List.repeat 1000 n).
   Next Obligation. now rewrite List.repeat_length. Qed.
 
-Definition silent_long_vector := 0.
- (* Vector.eqb _ Nat.eqb (long_vector 5000) (long_vector 5000). *)
+Definition silent_long_vector :=
+ Vector.eqb _ Nat.eqb (long_vector 5000) (long_vector 5000).
 
 (* Time Eval vm_compute in silent_long_vector. (* Blows up *) *)
 (* 1.23s *)
@@ -68,7 +68,7 @@ CertiCoq Eval -time sha_fast_noproofs.
 (* Executed in 0.037175 sec *)
 
 Time CertiCoq Eval sha_fast_noproofs.
-(* Finished transaction in 0.06 sec *)
+(* Finished transaction in 0.02 sec *)
 
 CertiCoq Eval -time sha_fast_noproofs.
 (* Executed in 0.045 sec *)
@@ -106,9 +106,9 @@ Definition vs_hard :=
 (* Blows up *) Time Eval vm_compute in vs_hard.
 *)
 
-(* CertiCoq Eval -time vs_hard. *)
+CertiCoq Eval -time vs_hard.
 (* Executed in 0.06s *)
-(* CertiCoq Eval -time vs_hard. *)
+CertiCoq Eval -time vs_hard.
 
 (* CertiCoq Eval -time vs_easy. *)
 (* Executed in 0.007s *)
diff --git a/benchmarks/lib/Binom.v b/benchmarks/lib/Binom.v
index b853a13c..23b9ba36 100755
--- a/benchmarks/lib/Binom.v
+++ b/benchmarks/lib/Binom.v
@@ -1,6 +1,4 @@
-Require Import Coq.Arith.Arith
-               Coq.Numbers.Natural.Peano.NPeano
-               List.
+Require Import Coq.Arith.Arith List.
 
 Import ListNotations.
 Import Nat. (* For 8.5.0 *)
diff --git a/benchmarks/lib/Makefile b/benchmarks/lib/Makefile
index 7012dfb2..8bd86989 100644
--- a/benchmarks/lib/Makefile
+++ b/benchmarks/lib/Makefile
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.17.0
+## GNUMakefile for Coq 8.19.1
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.17.0
+COQMAKEFILE_VERSION:=8.19.1
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -293,18 +293,26 @@ CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
 CAMLFLAGS+=$(OCAMLWARN)
 
 ifneq (,$(TIMING))
-TIMING_ARG=-time
-ifeq (after,$(TIMING))
-TIMING_EXT=after-timing
+  ifeq (after,$(TIMING))
+    TIMING_EXT=after-timing
+  else
+    ifeq (before,$(TIMING))
+      TIMING_EXT=before-timing
+    else
+      TIMING_EXT=timing
+    endif
+  endif
+  TIMING_ARG=-time-file $<.$(TIMING_EXT)
 else
-ifeq (before,$(TIMING))
-TIMING_EXT=before-timing
-else
-TIMING_EXT=timing
-endif
+  TIMING_ARG=
 endif
+
+ifneq (,$(PROFILING))
+  PROFILE_ARG=-profile $<.prof.json
+  PROFILE_ZIP=gzip $<.prof.json
 else
-TIMING_ARG=
+  PROFILE_ARG=
+  PROFILE_ZIP=true
 endif
 
 # Files #######################################################################
@@ -592,13 +600,24 @@ beautify: $(BEAUTYFILES)
 # There rules can be extended in Makefile.local
 # Extensions can't assume when they run.
 
+# We use $(file) to avoid generating a very long command string to pass to the shell
+# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux)
+# However Apple ships old make which doesn't have $(file) so we need a fallback
+$(file >.hasfile,1)
+HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi)
+
+MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\
+  $(shell rm -f .filestoinstall) \
+  $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall)))
+
 # findlib needs the package to not be installed, so we remove it before
 # installing it (see the call to findlib_remove)
 install: META
-	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+	@$(MKFILESTOINSTALL)
+	$(HIDE)code=0; for f in $$(cat .filestoinstall); do\
 	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
 	done; exit $$code
-	$(HIDE)for f in $(FILESTOINSTALL); do\
+	$(HIDE)for f in $$(cat .filestoinstall); do\
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
 	 if [ "$$?" != "0" -o -z "$$df" ]; then\
 	   echo SKIP "$$f" since it has no logical path;\
@@ -611,6 +630,7 @@ install: META
 	$(call findlib_remove)
 	$(call findlib_install, META $(FINDLIBFILESTOINSTALL))
 	$(HIDE)$(MAKE) install-extra -f "$(SELF)"
+	@rm -f .filestoinstall
 install-extra::
 	@# Extension point
 .PHONY: install install-extra
@@ -642,18 +662,20 @@ install-doc:: html mlihtml
 
 uninstall::
 	@# Extension point
+	@$(MKFILESTOINSTALL)
 	$(call findlib_remove)
-	$(HIDE)for f in $(FILESTOINSTALL); do \
+	$(HIDE)for f in $$(cat .filestoinstall); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
 	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf" ;\
 	done
-	$(HIDE)for f in $(FILESTOINSTALL); do \
+	$(HIDE)for f in $$(cat .filestoinstall); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
 	 echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\
 	 (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
 	done
+	@rm -f .filestoinstall
 
 .PHONY: uninstall
 
@@ -784,12 +806,6 @@ $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix
 	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \
 		-shared -o $@ $<
 
-ifneq (,$(TIMING))
-TIMING_EXTRA = > $<.$(TIMING_EXT)
-else
-TIMING_EXTRA =
-endif
-
 # can't make
 # https://www.gnu.org/software/make/manual/make.html#Static-Pattern
 # work with multiple target rules
@@ -800,12 +816,13 @@ ifneq (,$(filter grouped-target,$(.FEATURES)))
 define globvorule=
 
 # take care to $$ variables using $< etc
-  $(1).vo $(1).glob &: $(1).v | $(VDFILE)
-	$(SHOW)COQC $(1).v
-	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v $$(TIMING_EXTRA)
+  $(1).vo $(1).glob &: $(1).v | $$(VDFILE)
+	$$(SHOW)COQC $(1).v
+	$$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v
+	$$(HIDE)$$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
-	$(SHOW)COQNATIVE $(1).vo
-	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
+	$$(SHOW)COQNATIVE $(1).vo
+	$$(HIDE)$$(call TIMER,$(1).vo.native) $$(COQNATIVE) $$(COQLIBS) $(1).vo
 endif
 
 endef
@@ -813,7 +830,8 @@ else
 
 $(VOFILES): %.vo: %.v | $(VDFILE)
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
 	$(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@
diff --git a/bootstrap/certicoqc/Makefile b/bootstrap/certicoqc/Makefile
index 0e5d1c12..2b804e7a 100644
--- a/bootstrap/certicoqc/Makefile
+++ b/bootstrap/certicoqc/Makefile
@@ -2,7 +2,15 @@
 CCOMPILER := $(shell { command -v clang-11 || command -v clang || command -v gcc; } 2>/dev/null)
 # clang options
 CCOMPILEROPTS = -fPIC -fomit-frame-pointer -g -c -I . -I $(RUNTIME_DIR) -I ${OCAMLLIB} -w -Wno-everything -O2
+UNAME=$(shell uname -s)
+ifeq '$(UNAME)' 'Darwin'
+  SED= $(shell which gsed)
+  ifeq '$(SED)' ''
+   $(error "Must have gsed installed on MacOS, try e.g. brew install gsed")
+  endif
+else
 SED=`which gsed || which sed`
+endif
 
 # CompCert compiler
 CCOMPCOMPILER := $(CCOMPILER)
@@ -35,8 +43,12 @@ ifeq '$(CERTICOQ_CONFIG)' 'local'
 
   TESTCOQOPTS = $(COQOPTS)
 else
+ ifeq '$(CERTICOQ_CONFIG)' 'global'
   COQOPTS = -I . -Q theories CertiCoq.CertiCoqC
   TESTCOQOPTS = 
+ else
+  $(error "Must first set CERTICOQ_CONFIG by running ./configure.sh")
+ endif
 endif
 
 PKGS = -package coq-core,coq-core.clib,coq-core.config,coq-core.engine,coq-core.gramlib,coq-core.interp,coq-core.kernel,coq-core.lib,coq-core.library,coq-core.toplevel,coq-core.vernac,coq-core.plugins.ltac
@@ -127,4 +139,4 @@ install: theories/compile.vo certicoqc_plugin.cmxs
 
 .PHONY: plugin test
 
-.NOTPARALLEL:
\ No newline at end of file
+.NOTPARALLEL:
diff --git a/coq-certicoq.opam b/coq-certicoq.opam
index 5a55a30f..48be9ef9 100644
--- a/coq-certicoq.opam
+++ b/coq-certicoq.opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev+8.17"
+version: "dev+8.19"
 maintainer: "The CertiCoq Team"
 homepage: "https://certicoq.org/"
 dev-repo: "git+https://github.com/CertiCoq/certicoq"
@@ -33,12 +33,12 @@ depends: [
   "ocaml"
   "conf-clang"
   "stdlib-shims"
-  "coq" {>= "8.17" & < "8.18~"}
-  "coq-compcert" {= "3.12"}
-  "coq-equations" {= "1.3+8.17"}
-  "coq-metacoq-erasure-plugin" {= "8.17.dev"}
-  "coq-metacoq-safechecker-plugin" {= "8.17.dev"}
-  "coq-ext-lib" {>= "0.11.8"}
+  "coq" {>= "8.19" & < "8.20~"}
+  "coq-compcert" {= "3.13.1"}
+  "coq-equations" {= "1.3+8.19"}
+  "coq-metacoq-erasure-plugin" {= "1.3.1+8.19"}
+  "coq-metacoq-safechecker-plugin" {= "1.3.1+8.19"}
+  "coq-ext-lib" {>= "0.12"}
 ]
 
 synopsis: "A Verified Compiler for Gallina, Written in Gallina "
diff --git a/cplugin/CoqMsgFFI.v b/cplugin/CoqMsgFFI.v
index 3970c947..4a1b0f0a 100644
--- a/cplugin/CoqMsgFFI.v
+++ b/cplugin/CoqMsgFFI.v
@@ -11,4 +11,4 @@ CertiCoq Register [
   coq_msg_notice => "coq_msg_notice",
   coq_msg_debug => "coq_msg_debug",
   coq_user_error => "coq_user_error" ]
-Include [ "coq_c_ffi.h" "coq_ffi.h" as library ].
+Include [ Library "coq_c_ffi.h" "coq_ffi.h" ].
diff --git a/cplugin/Makefile.local b/cplugin/Makefile.local
index 8bb44a1f..668244e4 100644
--- a/cplugin/Makefile.local
+++ b/cplugin/Makefile.local
@@ -7,12 +7,13 @@ CAMLFLAGS+=-w -32 # Unused values
 CAMLFLAGS+=-w -39 # Unused rec flagss
 CAMLFLAGS+=-w -20 # Unused arguments
 CAMLFLAGS+=-w -60 # Unused functor arguments
-CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims
+CAMLPKGS += -package coq-metacoq-template-ocaml.plugin,stdlib-shims
 
 CC=$(shell which gcc || which clang-11)
 
 merlin-hook::
-		$(HIDE)echo 'FLG $(OPENS)' >> .merlin
+		$(HIDE)echo 'PKG coq-metacoq-template-ocaml.plugin' >> .merlin
+		$(HIDE)echo 'PKG stdlib-shims' >> .merlin
 
 get_ordinal.o: get_ordinal.c
 	$(CC) -c -o $@ -I runtime $<
diff --git a/cplugin/PrimFloats.v b/cplugin/PrimFloats.v
index 4c6b83a2..53649c20 100644
--- a/cplugin/PrimFloats.v
+++ b/cplugin/PrimFloats.v
@@ -20,4 +20,4 @@ CertiCoq Register [
   Coq.Floats.PrimFloat.of_uint63 => "prim_float_of_uint63" with tinfo,
   Coq.Floats.PrimFloat.next_up => "prim_float_next_up" with tinfo,
   Coq.Floats.PrimFloat.next_down => "prim_float_next_down" with tinfo ]
-Include [ "prim_floats.h" as library ].
+Include [ Library "prim_floats.h" ].
diff --git a/cplugin/PrimInt63.v b/cplugin/PrimInt63.v
index 33b3c9df..af7c511b 100644
--- a/cplugin/PrimInt63.v
+++ b/cplugin/PrimInt63.v
@@ -27,4 +27,4 @@ CertiCoq Register [
   Coq.Numbers.Cyclic.Int63.PrimInt63.lor => "prim_int63_lor", 
   Coq.Numbers.Cyclic.Int63.PrimInt63.lxor => "prim_int63_lxor"
 ]
-Include [ "prim_int63.h" as library ].
+Include [ Library "prim_int63.h" ].
diff --git a/cplugin/_CoqProject b/cplugin/_CoqProject
index 3277ed9a..b9d0cb38 100644
--- a/cplugin/_CoqProject
+++ b/cplugin/_CoqProject
@@ -38,37 +38,11 @@ static/printAST.ml
 static/printClight.ml
 static/printCsyntax.ml
 
-
+# `ls extraction/*.mli extraction/*.ml`
+extraction/AST.ml
+extraction/AST.mli
 extraction/all_Forall.ml
 extraction/all_Forall.mli
-# extraction/string2pos.mli
-# extraction/string2pos.ml
-# extraction/canonicalTries.mli
-# extraction/canonicalTries.ml
-extraction/fMapList.mli
-extraction/fMapList.ml
-extraction/decidableType.mli
-extraction/decidableType.ml
-extraction/fMapInterface.mli
-extraction/fMapInterface.ml
-extraction/fMapAVL.mli
-extraction/fMapAVL.ml
-extraction/fMapFacts.mli
-extraction/fMapFacts.ml
-extraction/envMap.mli
-extraction/envMap.ml
-extraction/pCUICWfEnv.mli
-extraction/pCUICWfEnv.ml
-extraction/pCUICWfEnvImpl.mli
-extraction/pCUICWfEnvImpl.ml
-extraction/typing0.mli
-extraction/typing0.ml
-extraction/environmentTyping.mli
-extraction/environmentTyping.ml
-extraction/astUtils.mli
-extraction/astUtils.ml
-extraction/etaExpand.mli
-extraction/etaExpand.ml
 extraction/archi.ml
 extraction/archi.mli
 extraction/ascii.ml
@@ -77,56 +51,54 @@ extraction/ast0.ml
 extraction/ast0.mli
 extraction/astCommon.ml
 extraction/astCommon.mli
-extraction/AST.ml
-extraction/AST.mli
+extraction/astUtils.ml
+extraction/astUtils.mli
 extraction/basicAst.ml
 extraction/basicAst.mli
 extraction/basics.ml
 extraction/basics.mli
-extraction/binarySingleNaN.mli
-extraction/binarySingleNaN.ml
-extraction/binary.ml
-extraction/binary.mli
 extraction/binInt.ml
 extraction/binInt.mli
-extraction/binNatDef.ml
-extraction/binNatDef.mli
 extraction/binNat.ml
 extraction/binNat.mli
+extraction/binNatDef.ml
+extraction/binNatDef.mli
 extraction/binNums.ml
 extraction/binNums.mli
-extraction/binPosDef.ml
-extraction/binPosDef.mli
 extraction/binPos.ml
 extraction/binPos.mli
+extraction/binPosDef.ml
+extraction/binPosDef.mli
+extraction/binary.ml
+extraction/binary.mli
+extraction/binarySingleNaN.ml
+extraction/binarySingleNaN.mli
 extraction/bits.ml
 extraction/bits.mli
 extraction/bool.ml
 extraction/bool.mli
-extraction/byte.mli
 extraction/byte.ml
-extraction/byte0.mli
+extraction/byte.mli
 extraction/byte0.ml
-extraction/byteCompare.mli
+extraction/byte0.mli
 extraction/byteCompare.ml
-extraction/bytestring.mli
+extraction/byteCompare.mli
 extraction/bytestring.ml
+extraction/bytestring.mli
+extraction/cRelationClasses.ml
+extraction/cRelationClasses.mli
 extraction/classes1.ml
 extraction/classes1.mli
 extraction/classes2.ml
 extraction/classes2.mli
-extraction/ctypesdefs.mli
-extraction/ctypesdefs.ml
 extraction/clight.ml
 extraction/clight.mli
 extraction/closure_conversion.ml
 extraction/closure_conversion.mli
-extraction/compile0.ml
-extraction/compile0.mli
-# extraction/compile1.ml
-# extraction/compile1.mli
 extraction/compM.ml
 extraction/compM.mli
+extraction/compile0.ml
+extraction/compile0.mli
 extraction/config0.ml
 extraction/config0.mli
 extraction/cop.ml
@@ -135,134 +107,126 @@ extraction/coqlib0.ml
 extraction/coqlib0.mli
 extraction/cps.ml
 extraction/cps.mli
-extraction/cps_proto_univ.mli
-extraction/cps_proto_univ.ml
 extraction/cps_proto.ml
 extraction/cps_proto.mli
+extraction/cps_proto_univ.ml
+extraction/cps_proto_univ.mli
 extraction/cps_show.ml
 extraction/cps_show.mli
 extraction/cps_util.ml
 extraction/cps_util.mli
 extraction/csyntax.ml
 extraction/csyntax.mli
-extraction/primInt63.mli
-extraction/primInt63.ml
-extraction/uint0.mli
-extraction/uint0.ml
-extraction/primitive.mli
-extraction/primitive.ml
-extraction/pCUICPrimitive.mli
-extraction/pCUICPrimitive.ml
 extraction/ctx.ml
 extraction/ctx.mli
 extraction/ctypes.ml
 extraction/ctypes.mli
+extraction/ctypesdefs.ml
+extraction/ctypesdefs.mli
 extraction/datatypes.ml
 extraction/datatypes.mli
 extraction/dead_param_elim.ml
 extraction/dead_param_elim.mli
+extraction/decidableClass.ml
+extraction/decidableClass.mli
+extraction/decidableType.ml
+extraction/decidableType.mli
 extraction/decimal.ml
 extraction/decimal.mli
-extraction/show.mli
-extraction/show.ml
-extraction/transform.mli
-extraction/transform.ml
-extraction/ePrimitive.mli
-extraction/ePrimitive.ml
 extraction/eAst.ml
 extraction/eAst.mli
-extraction/eGlobalEnv.mli
-extraction/eGlobalEnv.ml
 extraction/eAstUtils.ml
 extraction/eAstUtils.mli
-extraction/eEnvMap.mli
+extraction/eBeta.ml
+extraction/eBeta.mli
+extraction/eCSubst.ml
+extraction/eCSubst.mli
+extraction/eCoInductiveToInductive.ml
+extraction/eCoInductiveToInductive.mli
+extraction/eConstructorsAsBlocks.ml
+extraction/eConstructorsAsBlocks.mli
 extraction/eEnvMap.ml
+extraction/eEnvMap.mli
+extraction/eEtaExpanded.ml
+extraction/eEtaExpanded.mli
+extraction/eGlobalEnv.ml
+extraction/eGlobalEnv.mli
+extraction/eInduction.ml
+extraction/eInduction.mli
+extraction/eInlineProjections.ml
+extraction/eInlineProjections.mli
+extraction/eInlining.ml
+extraction/eInlining.mli
 extraction/eLiftSubst.ml
 extraction/eLiftSubst.mli
-extraction/ePretty.mli
-extraction/ePretty.ml
-extraction/resultMonad.mli
-extraction/resultMonad.ml
-extraction/exAst.mli
-extraction/exAst.ml
-extraction/fin.mli
-extraction/fin.ml
-extraction/vectorDef.mli
-extraction/vectorDef.ml
-extraction/vector.mli
-extraction/vector.ml
-extraction/optimize.mli
-extraction/optimize.ml
-extraction/optimizeCorrectness.mli
-extraction/optimizeCorrectness.ml
-extraction/eCSubst.ml
-extraction/eCSubst.mli
-extraction/eWellformed.mli
-extraction/eWellformed.ml
-extraction/eProgram.mli
-extraction/eProgram.ml
-extraction/eWcbvEval.mli
-extraction/eWcbvEval.ml
-extraction/environment.ml
-extraction/environment.mli
 extraction/eOptimizePropDiscr.ml
 extraction/eOptimizePropDiscr.mli
-extraction/eInduction.ml
-extraction/eInduction.mli
-extraction/eSpineView.ml
-extraction/eSpineView.mli
-extraction/eEtaExpanded.ml
-extraction/eEtaExpanded.mli
+extraction/ePretty.ml
+extraction/ePretty.mli
+extraction/ePrimitive.ml
+extraction/ePrimitive.mli
+extraction/eProgram.ml
+extraction/eProgram.mli
 extraction/eRemoveParams.ml
 extraction/eRemoveParams.mli
-extraction/eInlineProjections.mli
-extraction/eInlineProjections.ml
-extraction/eConstructorsAsBlocks.mli
-extraction/eConstructorsAsBlocks.ml
-extraction/eUnboxing.mli
-extraction/eUnboxing.ml
-extraction/eInlining.mli
-extraction/eInlining.ml
-extraction/eBeta.mli
-extraction/eBeta.ml
-extraction/eCoInductiveToInductive.mli
-extraction/eCoInductiveToInductive.ml
-extraction/eReorderCstrs.mli
 extraction/eReorderCstrs.ml
-extraction/eTransform.mli
+extraction/eReorderCstrs.mli
+extraction/eSpineView.ml
+extraction/eSpineView.mli
 extraction/eTransform.ml
+extraction/eTransform.mli
+extraction/eUnboxing.ml
+extraction/eUnboxing.mli
+extraction/eWcbvEval.ml
+extraction/eWcbvEval.mli
+extraction/eWellformed.ml
+extraction/eWellformed.mli
+extraction/envMap.ml
+extraction/envMap.mli
+extraction/environment.ml
+extraction/environment.mli
+extraction/environmentTyping.ml
+extraction/environmentTyping.mli
 extraction/eqDecInstances.ml
 extraction/eqDecInstances.mli
 extraction/equalities.ml
 extraction/equalities.mli
+extraction/erasure.ml
+extraction/erasure.mli
+extraction/erasure0.ml
+extraction/erasure0.mli
 extraction/erasureFunction.ml
 extraction/erasureFunction.mli
-extraction/erasureFunctionProperties.mli
 extraction/erasureFunctionProperties.ml
-extraction/optimizePropDiscr.mli
-extraction/optimizePropDiscr.ml
-extraction/extractionCorrectness.mli
-extraction/extractionCorrectness.ml
-extraction/erasure0.mli
-extraction/erasure0.ml
-extraction/erasure.ml
-extraction/erasure.mli
+extraction/erasureFunctionProperties.mli
 extraction/errors0.ml
 extraction/errors0.mli
-extraction/cRelationClasses.mli
-extraction/cRelationClasses.ml
-# extraction/eGlobalEnv.ml
-# extraction/eGlobalEnv.mli
+extraction/etaExpand.ml
+extraction/etaExpand.mli
 extraction/eval.ml
 extraction/eval.mli
+extraction/exAst.ml
+extraction/exAst.mli
 extraction/exceptionMonad.ml
 extraction/exceptionMonad.mli
 extraction/expression.ml
 extraction/expression.mli
 extraction/extract.ml
 extraction/extract.mli
+extraction/extractionCorrectness.ml
+extraction/extractionCorrectness.mli
+extraction/fMapAVL.ml
+extraction/fMapAVL.mli
+extraction/fMapFacts.ml
+extraction/fMapFacts.mli
+extraction/fMapInterface.ml
+extraction/fMapInterface.mli
+extraction/fMapList.ml
+extraction/fMapList.mli
 extraction/ffi.ml
 extraction/ffi.mli
+extraction/fin.ml
+extraction/fin.mli
 extraction/floatOps.ml
 extraction/floatOps.mli
 extraction/floats.ml
@@ -279,32 +243,30 @@ extraction/hexadecimal.ml
 extraction/hexadecimal.mli
 extraction/hoisting.ml
 extraction/hoisting.mli
-extraction/identifiers.ml
-extraction/identifiers.mli
 extraction/iEEE754_extra.ml
 extraction/iEEE754_extra.mli
-extraction/int0.mli
-extraction/int0.ml
+extraction/identifiers.ml
+extraction/identifiers.mli
 extraction/init.ml
 extraction/init.mli
-extraction/inline_letapp.ml
-extraction/inline_letapp.mli
 extraction/inline.ml
 extraction/inline.mli
+extraction/inline_letapp.ml
+extraction/inline_letapp.mli
+extraction/int0.ml
+extraction/int0.mli
 extraction/integers.ml
 extraction/integers.mli
 extraction/kernames.ml
 extraction/kernames.mli
-extraction/lambdaBoxMut_to_LambdaBoxLocal.ml
-extraction/lambdaBoxMut_to_LambdaBoxLocal.mli
-extraction/lambdaBoxLocal_to_LambdaANF.ml
-extraction/lambdaBoxLocal_to_LambdaANF.mli
-extraction/optionMonad.mli
-extraction/optionMonad.ml
 extraction/lambdaANF_to_Clight.ml
 extraction/lambdaANF_to_Clight.mli
 extraction/lambdaANF_to_Clight_stack.ml
 extraction/lambdaANF_to_Clight_stack.mli
+extraction/lambdaBoxLocal_to_LambdaANF.ml
+extraction/lambdaBoxLocal_to_LambdaANF.mli
+extraction/lambdaBoxMut_to_LambdaBoxLocal.ml
+extraction/lambdaBoxMut_to_LambdaBoxLocal.mli
 extraction/lambda_lifting.ml
 extraction/lambda_lifting.mli
 extraction/list0.ml
@@ -313,46 +275,22 @@ extraction/list_util.ml
 extraction/list_util.mli
 extraction/logic0.ml
 extraction/logic0.mli
-extraction/maps.ml
-extraction/maps.mli
-extraction/utils.mli
-extraction/utils.ml
-extraction/maps_util.ml
-extraction/maps_util.mli
-extraction/map_util.ml
-extraction/map_util.mli
-extraction/reflectEq.mli
-extraction/reflectEq.ml
-extraction/mCString.mli
-extraction/mCString.ml
 extraction/mCCompare.ml
 extraction/mCCompare.mli
 extraction/mCList.ml
 extraction/mCList.mli
-extraction/mCReflect.ml
-extraction/mCReflect.mli
 extraction/mCOption.ml
 extraction/mCOption.mli
 extraction/mCPrelude.ml
 extraction/mCPrelude.mli
 extraction/mCProd.ml
 extraction/mCProd.mli
-extraction/reflect.mli
-extraction/reflect.ml
-extraction/memdata.ml
-extraction/memdata.mli
-extraction/memory.ml
-extraction/memory.mli
-extraction/memtype.ml
-extraction/memtype.mli
-extraction/monad0.ml
-extraction/monad0.mli
-# extraction/monadExc.ml
-# extraction/monadExc.mli
-extraction/monadState.ml
-extraction/monadState.mli
-extraction/monad_utils.ml
-extraction/monad_utils.mli
+extraction/mCReflect.ml
+extraction/mCReflect.mli
+extraction/mCString.ml
+extraction/mCString.mli
+extraction/mSetAVL.ml
+extraction/mSetAVL.mli
 extraction/mSetDecide.ml
 extraction/mSetDecide.mli
 extraction/mSetFacts.ml
@@ -361,28 +299,52 @@ extraction/mSetInterface.ml
 extraction/mSetInterface.mli
 extraction/mSetList.ml
 extraction/mSetList.mli
-extraction/mSetAVL.mli
-extraction/mSetAVL.ml
 extraction/mSetProperties.ml
 extraction/mSetProperties.mli
 extraction/mSetRBT.ml
 extraction/mSetRBT.mli
+extraction/map_util.ml
+extraction/map_util.mli
+extraction/maps.ml
+extraction/maps.mli
+extraction/maps_util.ml
+extraction/maps_util.mli
+extraction/memdata.ml
+extraction/memdata.mli
+extraction/memory.ml
+extraction/memory.mli
+extraction/memtype.ml
+extraction/memtype.mli
+extraction/monad0.ml
+extraction/monad0.mli
+extraction/monadState.ml
+extraction/monadState.mli
+extraction/monad_utils.ml
+extraction/monad_utils.mli
 extraction/nat0.ml
 extraction/nat0.mli
 extraction/number0.ml
 extraction/number0.mli
+extraction/optimize.ml
+extraction/optimize.mli
+extraction/optimizeCorrectness.ml
+extraction/optimizeCorrectness.mli
+extraction/optimizePropDiscr.ml
+extraction/optimizePropDiscr.mli
+extraction/optionMonad.ml
+extraction/optionMonad.mli
 extraction/orderedType0.ml
 extraction/orderedType0.mli
 extraction/orderedTypeAlt.ml
 extraction/orderedTypeAlt.mli
+extraction/orders.ml
+extraction/orders.mli
 extraction/ordersEx.ml
 extraction/ordersEx.mli
 extraction/ordersFacts.ml
 extraction/ordersFacts.mli
 extraction/ordersLists.ml
 extraction/ordersLists.mli
-extraction/orders.ml
-extraction/orders.mli
 extraction/ordersTac.ml
 extraction/ordersTac.mli
 extraction/pCUICAst.ml
@@ -391,57 +353,68 @@ extraction/pCUICAstUtils.ml
 extraction/pCUICAstUtils.mli
 extraction/pCUICCases.ml
 extraction/pCUICCases.mli
+extraction/pCUICEqualityDec.ml
+extraction/pCUICEqualityDec.mli
 extraction/pCUICErrors.ml
 extraction/pCUICErrors.mli
 extraction/pCUICExpandLets.ml
 extraction/pCUICExpandLets.mli
-extraction/pCUICEqualityDec.mli
-extraction/pCUICEqualityDec.ml
 extraction/pCUICNormal.ml
 extraction/pCUICNormal.mli
 extraction/pCUICPosition.ml
 extraction/pCUICPosition.mli
-# extraction/pCUICPrimitive.ml
-# extraction/pCUICPrimitive.mli
+extraction/pCUICPrimitive.ml
+extraction/pCUICPrimitive.mli
+extraction/pCUICProgram.ml
+extraction/pCUICProgram.mli
 extraction/pCUICSafeReduce.ml
 extraction/pCUICSafeReduce.mli
 extraction/pCUICSafeRetyping.ml
 extraction/pCUICSafeRetyping.mli
+extraction/pCUICTransform.ml
+extraction/pCUICTransform.mli
 extraction/pCUICTyping.ml
 extraction/pCUICTyping.mli
-extraction/pCUICProgram.mli
-extraction/pCUICProgram.ml
-extraction/pCUICTransform.mli
-extraction/pCUICTransform.ml
-
+extraction/pCUICWfEnv.ml
+extraction/pCUICWfEnv.mli
+extraction/pCUICWfEnvImpl.ml
+extraction/pCUICWfEnvImpl.mli
+extraction/pOrderedType.ml
+extraction/pOrderedType.mli
 extraction/peanoNat.ml
 extraction/peanoNat.mli
 extraction/pipeline.ml
 extraction/pipeline.mli
 extraction/pipeline_utils.ml
 extraction/pipeline_utils.mli
-extraction/pOrderedType.ml
-extraction/pOrderedType.mli
 extraction/primFloat.ml
 extraction/primFloat.mli
-# extraction/primInt63.ml
-# extraction/primInt63.mli
-extraction/prototype.ml
-extraction/prototype.mli
+extraction/primInt63.ml
+extraction/primInt63.mli
+extraction/primitive.ml
+extraction/primitive.mli
 extraction/proto_util.ml
 extraction/proto_util.mli
+extraction/prototype.ml
+extraction/prototype.mli
 extraction/randyPrelude.ml
 extraction/randyPrelude.mli
+extraction/reflect.ml
+extraction/reflect.mli
+extraction/reflectEq.ml
+extraction/reflectEq.mli
 extraction/rename.ml
 extraction/rename.mli
+extraction/resultMonad.ml
+extraction/resultMonad.mli
 extraction/rewriting.ml
 extraction/rewriting.mli
 extraction/round.ml
 extraction/round.mli
-# extraction/safeTemplateChecker.ml
-# extraction/safeTemplateChecker.mli
 extraction/set_util.ml
 extraction/set_util.mli
+extraction/show.ml
+extraction/show.mli
 extraction/shrink_cps.ml
 extraction/shrink_cps.mli
 extraction/signature.ml
@@ -460,36 +433,46 @@ extraction/stateMonad.ml
 extraction/stateMonad.mli
 extraction/string0.ml
 extraction/string0.mli
-extraction/templateEnvMap.mli
 extraction/templateEnvMap.ml
+extraction/templateEnvMap.mli
 extraction/templateProgram.ml
 extraction/templateProgram.mli
 extraction/templateToPCUIC.ml
 extraction/templateToPCUIC.mli
+extraction/toplevel.ml
+extraction/toplevel.mli
 extraction/toplevel0.ml
 extraction/toplevel0.mli
 extraction/toplevel1.ml
 extraction/toplevel1.mli
 extraction/toplevel2.ml
 extraction/toplevel2.mli
-# extraction/topleveLambdaBoxMut.ml
-# extraction/topleveLambdaBoxMut.mli
-extraction/toplevel.ml
-extraction/toplevel.mli
+extraction/transform.ml
+extraction/transform.mli
+extraction/typing0.ml
+extraction/typing0.mli
 extraction/uGraph0.ml
 extraction/uGraph0.mli
-# extraction/uint0.ml
-# extraction/uint0.mli
+extraction/uint0.ml
+extraction/uint0.mli
 extraction/uncurry.ml
 extraction/uncurry.mli
 extraction/uncurry_proto.ml
 extraction/uncurry_proto.mli
 extraction/universes0.ml
 extraction/universes0.mli
+extraction/utils.ml
+extraction/utils.mli
 extraction/values0.ml
 extraction/values0.mli
+extraction/vector.ml
+extraction/vector.mli
+extraction/vectorDef.ml
+extraction/vectorDef.mli
 extraction/wGraph.ml
 extraction/wGraph.mli
+extraction/wf.ml
+extraction/wf.mli
 extraction/zArith_dec.ml
 extraction/zArith_dec.mli
 extraction/zbits.ml
diff --git a/cplugin/certicoq.ml b/cplugin/certicoq.ml
index de1e74c5..632e97a5 100644
--- a/cplugin/certicoq.ml
+++ b/cplugin/certicoq.ml
@@ -135,19 +135,17 @@ let fix_quoted_program (p : Ast0.Env.program) =
 
 end
 
+
 let get_stringopt_option key =
   let open Goptions in
-  let tables = get_tables () in
-  try
-    let _ = OptionMap.find key tables in
-    fun () ->
-      let tables = get_tables () in
-      let opt = OptionMap.find key tables in
-      match opt.opt_value with
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
       | StringOptValue b -> b
       | _ -> assert false
-  with Not_found ->
-    declare_stringopt_option_and_ref ~depr:false ~key
+      end
+  | None ->
+    (declare_stringopt_option_and_ref ~key ~value:None ()).get
 
 let get_build_dir_opt =
   get_stringopt_option ["CertiCoq"; "Build"; "Directory"]
@@ -676,8 +674,8 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n  ++ str" while running " ++ str cmd)
     
   type reifyable_type =
-  | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list
-  | IsPrimitive of Names.Constant.t * Univ.Instance.t * Constr.t list
+  | IsInductive of Names.inductive * UVars.Instance.t * Constr.t list
+  | IsPrimitive of Names.Constant.t * UVars.Instance.t * Constr.t list
   
   let type_of_reifyable_type = function
     | IsInductive (hd, u, args) -> Term.applistc (Constr.mkIndU ((hd, u))) args
@@ -715,7 +713,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let hd, args = EConstr.decompose_app sigma hnf in
       match EConstr.kind sigma hd with
       | Const (c, u) when Environ.is_primitive_type env c -> 
-        IsPrimitive (c, EConstr.EInstance.kind sigma u, List.map EConstr.Unsafe.to_constr args)
+        IsPrimitive (c, EConstr.EInstance.kind sigma u, CArray.map_to_list EConstr.Unsafe.to_constr args)
       | _ -> CErrors.user_err 
         Pp.(str"Cannot reify values of non-inductive or non-primitive type: " ++ 
           Printer.pr_econstr_env env sigma ty)
diff --git a/cplugin/certicoq_vanilla_plugin.mlpack b/cplugin/certicoq_vanilla_plugin.mlpack
index ab7d90fb..3b87bd4e 100644
--- a/cplugin/certicoq_vanilla_plugin.mlpack
+++ b/cplugin/certicoq_vanilla_plugin.mlpack
@@ -7,11 +7,13 @@ Caml_nat
 Caml_bool
 Caml_option
 Caml_comparison
+DecidableClass
 Bool
 Equalities
 Decimal
 Hexadecimal
 Nat0
+Wf
 List0
 PeanoNat
 Specif
diff --git a/cplugin/g_certicoq_vanilla.mlg b/cplugin/g_certicoq_vanilla.mlg
index 9cf0e539..eddffe4a 100644
--- a/cplugin/g_certicoq_vanilla.mlg
+++ b/cplugin/g_certicoq_vanilla.mlg
@@ -82,8 +82,8 @@ END
 
 VERNAC ARGUMENT EXTEND vanilla_cinclude
 | [ string(str) ] -> { FromRelativePath str }
-| [ string(str) "as" "absolute" ] -> { FromAbsolutePath str }
-| [ string(str) string_opt(str') "as" "library" ] -> { FromLibrary (str, str') }
+| [ "Absolute" string(str) ] -> { FromAbsolutePath str }
+| [ "Library" string(str) string_opt(str') ] -> { FromLibrary (str, str') }
 END
 
 VERNAC COMMAND EXTEND CertiCoq_Register CLASSIFIED AS SIDEFF
diff --git a/cplugin/plugin_utils.ml b/cplugin/plugin_utils.ml
index 07ee6c49..fbf46a16 100644
--- a/cplugin/plugin_utils.ml
+++ b/cplugin/plugin_utils.ml
@@ -3,20 +3,18 @@ open Names
 open Pp
 open Caml_bytestring
 
+  
 let debug_opt =
-   let open Goptions in
-   let key = ["CertiCoq"; "Debug"] in
-   let tables = get_tables () in
-   try
-     let _ = OptionMap.find key tables in
-     fun () ->
-       let tables = get_tables () in
-       let opt = OptionMap.find key tables in
-       match opt.opt_value with
-       | BoolValue b -> b
-       | _ -> assert false
-   with Not_found ->
-   declare_bool_option_and_ref ~depr:false ~key ~value:false
+  let open Goptions in
+  let key = ["CertiCoq"; "Debug"] in
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
+      | BoolValue b -> b
+      | _ -> assert false
+      end
+  | None ->
+   (declare_bool_option_and_ref ~key ~value:false ()).get
  
  let debug (m : unit ->Pp.t) =
    if debug_opt () then
diff --git a/cplugin/runtime/gc_stack.c b/cplugin/runtime/gc_stack.c
index f380cf1e..0ef06be3 100644
--- a/cplugin/runtime/gc_stack.c
+++ b/cplugin/runtime/gc_stack.c
@@ -207,6 +207,7 @@ void forward (value *from_start,  /* beginning of from-space */
         /* printf("New %lld\n", newv); */
         /* if (*p == 73832) printf("Found it\n"); */
         if (depth>0)
+	  if (!No_scan(Tag_hd(hd)))
           for (i=0; i<sz; i++)
             forward(from_start, from_limit, next, &Field(newv,i), depth-1);
       }
@@ -227,7 +228,7 @@ void forward_remset (struct space *from,  /* descriptor of from-space */
       forward(from_start, from_limit, next, p, DEPTH);
       newp= *p;
       if (oldp!=newp)
-          *(--to->limit) = (value)q;
+          *(--to->limit) = (value)p;
     }
     q++;
   }
diff --git a/cplugin/tm_util.ml b/cplugin/tm_util.ml
index 73c9a9c5..b1f54671 100644
--- a/cplugin/tm_util.ml
+++ b/cplugin/tm_util.ml
@@ -4,20 +4,17 @@ let contrib_name = "template-coq"
 
 (* This allows to load template_plugin and the extractable plugin at the same time 
   while have option settings apply to both *)
-  let timing_opt =
+let timing_opt =
   let open Goptions in
   let key = ["MetaCoq"; "Timing"] in
-  let tables = get_tables () in
-  try 
-    let _ = OptionMap.find key tables in
-    fun () -> 
-      let tables = get_tables () in
-      let opt = OptionMap.find key tables in
-      match opt.opt_value with
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
       | BoolValue b -> b
       | _ -> assert false
-  with Not_found ->
-    declare_bool_option_and_ref ~depr:false ~key ~value:false
+      end
+  | None ->
+    (declare_bool_option_and_ref ~key ~value:false ()).get
 
 let time prefix f x =
   if timing_opt () then 
@@ -31,23 +28,22 @@ let time prefix f x =
 let debug_opt =
   let open Goptions in
   let key = ["MetaCoq"; "Debug"] in
-  let tables = get_tables () in
-  try 
-    let _ = OptionMap.find key tables in
-    fun () -> 
-      let tables = get_tables () in
-      let opt = OptionMap.find key tables in
-      match opt.opt_value with
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
       | BoolValue b -> b
       | _ -> assert false
-  with Not_found ->
-  declare_bool_option_and_ref ~depr:false ~key ~value:false
+      end
+  | None ->
+    (declare_bool_option_and_ref ~key ~value:false ()).get
 
 let debug (m : unit ->Pp.t) =
   if debug_opt () then
     Feedback.(msg_debug (m ()))
   else
     ()
+
+
 type ('a,'b) sum =
   Left of 'a | Right of 'b
 
@@ -134,15 +130,15 @@ module CaseCompat =
     in
     instantiate (Array.length nas - 1) ctx
 
-  let case_predicate_context_gen mip ci u paramsubst nas =
-    let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
-    let self =
-      let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
-      let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in
-      mkApp (mkIndU (ci.ci_ind, inst), args)
-    in
-    let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
-    instantiate_context u paramsubst nas realdecls
+    let case_predicate_context_gen mip ci u paramsubst nas =
+      let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+      let self =
+        let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
+        let inst = UVars.Instance.abstract_instance (UVars.Instance.length u) in
+        mkApp (mkIndU (ci.ci_ind, inst), args)
+      in
+      let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
+      instantiate_context u paramsubst nas realdecls
 
   let case_predicate_context env ci u params nas =
     let mib = Environ.lookup_mind (fst ci.ci_ind) env in
diff --git a/libraries/CpdtTactics.v b/libraries/CpdtTactics.v
index af1c53a8..92267223 100644
--- a/libraries/CpdtTactics.v
+++ b/libraries/CpdtTactics.v
@@ -108,7 +108,7 @@ Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
 Ltac rewriter := autorewrite with core in *; rewriterP.
 
 (** This one is just so darned useful, let's add it as a hint here. *)
-Global Hint Rewrite app_ass : core.
+Global Hint Rewrite app_assoc : core.
 
 (** Devious marker predicate to use for encoding state within proof goals *)
 Definition done (T : Type) (x : T) := True.
@@ -197,7 +197,7 @@ Ltac crush' lemmas invOne :=
       end;
       sintuition; rewriter; sintuition;
       (** End with a last attempt to prove an arithmetic fact with [lia], or prove any sort of fact in a context that is contradictory by reasoning that [lia] can do. *)
-      try lia; try (elimtype False; lia)).
+      try lia; try (exfalso; lia)).
 
 (** [crush] instantiates [crush'] with the simplest possible parameters. *)
 Ltac crush := crush' false fail.
diff --git a/libraries/HashMap.v b/libraries/HashMap.v
index c67e69dd..fe09cf65 100755
--- a/libraries/HashMap.v
+++ b/libraries/HashMap.v
@@ -44,7 +44,7 @@ Module MakeHashMap (D: UsualOrderedType) <:
   Definition t := t'.
   Lemma norepet_empty: norepet nil.
   Proof. hnf; intros.
-         elimtype False; clear - H. induction i; inversion H.
+         exfalso; clear - H. induction i; inversion H.
   Qed.     
   Definition empty := Make _ norepet_empty.
   Definition get (i: index) (m: t) : option Domain.t := 
diff --git a/plugin/CoqMsgFFI.v b/plugin/CoqMsgFFI.v
index 89298a0f..c9f37d37 100644
--- a/plugin/CoqMsgFFI.v
+++ b/plugin/CoqMsgFFI.v
@@ -11,4 +11,4 @@ CertiCoq Register [
   coq_msg_notice => "coq_msg_notice",
   coq_msg_debug => "coq_msg_debug",
   coq_user_error => "coq_user_error" ]
-Include [ "coq_c_ffi.h" "coq_ffi.h" as library ].
+Include [ Library "coq_c_ffi.h" "coq_ffi.h" ].
diff --git a/plugin/Loader.v b/plugin/Loader.v
index 3abcd67d..c28f43c6 100644
--- a/plugin/Loader.v
+++ b/plugin/Loader.v
@@ -1 +1,2 @@
+Set Debug "backtrace".
 Declare ML Module "coq-certicoq.plugin".
\ No newline at end of file
diff --git a/plugin/Makefile.local b/plugin/Makefile.local
index f35e5adc..c7d05f3d 100644
--- a/plugin/Makefile.local
+++ b/plugin/Makefile.local
@@ -1,6 +1,4 @@
 COQ_SRC_SUBDIRS+=user-contrib/MetaCoq/Template
-# OPENS=-open Metacoq_template_plugin
-CAMLFLAGS+=$(OPENS)
 CAMLFLAGS+=-w -33 # Unused opens
 CAMLFLAGS+=-w -34 # Unused type program
 CAMLFLAGS+=-w -32 # Unused values
@@ -9,15 +7,18 @@ CAMLFLAGS+=-w -20 # Unused arguments
 CAMLFLAGS+=-w -60 # Unused functor arguments
 CAMLFLAGS+=-w -8 # Non-exhaustive matches produced by extraction
 CAMLFLAGS+=-w -37 # Unused constructor
-
-CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims
+CAMLPKGS += -package coq-metacoq-template-ocaml.plugin,stdlib-shims
 
 CC=$(shell which gcc || which clang-11)
 
 merlin-hook::
-		$(HIDE)echo 'FLG $(OPENS)' >> .merlin
+		$(HIDE)echo 'PKG coq-metacoq-template-ocaml.plugin' >> .merlin
+		$(HIDE)echo 'PKG stdlib-shims' >> .merlin
 
 get_ordinal.o: get_ordinal.c
 	$(CC) -c -o $@ -I runtime $<
 
-certicoq_vanilla_plugin.cmxs: get_ordinal.o
\ No newline at end of file
+certicoq_vanilla_plugin.cmxs: get_ordinal.o
+
+install-extra::
+	make -C runtime install
\ No newline at end of file
diff --git a/plugin/PrimFloats.v b/plugin/PrimFloats.v
index 0b61a2fb..5901d6be 100644
--- a/plugin/PrimFloats.v
+++ b/plugin/PrimFloats.v
@@ -21,4 +21,4 @@ CertiCoq Register [
   Coq.Floats.PrimFloat.of_uint63 => "prim_float_of_uint63" with tinfo,
   Coq.Floats.PrimFloat.next_up => "prim_float_next_up" with tinfo,
   Coq.Floats.PrimFloat.next_down => "prim_float_next_down" with tinfo ]
-Include [ "prim_floats.h" as library ].
+Include [ Library "prim_floats.h"  ].
diff --git a/plugin/PrimInt63.v b/plugin/PrimInt63.v
index d4e0a757..b0e8f9a3 100644
--- a/plugin/PrimInt63.v
+++ b/plugin/PrimInt63.v
@@ -30,4 +30,4 @@ CertiCoq Register [
   Coq.Numbers.Cyclic.Int63.PrimInt63.lor => "prim_int63_lor", 
   Coq.Numbers.Cyclic.Int63.PrimInt63.lxor => "prim_int63_lxor"
 ]
-Include [ "prim_int63.h" as library ].
+Include [ Library "prim_int63.h" ].
diff --git a/plugin/_CoqProject b/plugin/_CoqProject
index 722b3b76..6c77301f 100644
--- a/plugin/_CoqProject
+++ b/plugin/_CoqProject
@@ -31,37 +31,11 @@ static/printAST.ml
 static/printClight.ml
 static/printCsyntax.ml
 
-
+# `ls extraction/*.mli extraction/*.ml`
+extraction/AST.ml
+extraction/AST.mli
 extraction/all_Forall.ml
 extraction/all_Forall.mli
-# extraction/string2pos.mli
-# extraction/string2pos.ml
-# extraction/canonicalTries.mli
-# extraction/canonicalTries.ml
-extraction/fMapList.mli
-extraction/fMapList.ml
-extraction/decidableType.mli
-extraction/decidableType.ml
-extraction/fMapInterface.mli
-extraction/fMapInterface.ml
-extraction/fMapAVL.mli
-extraction/fMapAVL.ml
-extraction/fMapFacts.mli
-extraction/fMapFacts.ml
-extraction/envMap.mli
-extraction/envMap.ml
-extraction/pCUICWfEnv.mli
-extraction/pCUICWfEnv.ml
-extraction/pCUICWfEnvImpl.mli
-extraction/pCUICWfEnvImpl.ml
-extraction/typing0.mli
-extraction/typing0.ml
-extraction/environmentTyping.mli
-extraction/environmentTyping.ml
-extraction/astUtils.mli
-extraction/astUtils.ml
-extraction/etaExpand.mli
-extraction/etaExpand.ml
 extraction/archi.ml
 extraction/archi.mli
 extraction/ascii.ml
@@ -70,56 +44,54 @@ extraction/ast0.ml
 extraction/ast0.mli
 extraction/astCommon.ml
 extraction/astCommon.mli
-extraction/AST.ml
-extraction/AST.mli
+extraction/astUtils.ml
+extraction/astUtils.mli
 extraction/basicAst.ml
 extraction/basicAst.mli
 extraction/basics.ml
 extraction/basics.mli
-extraction/binarySingleNaN.mli
-extraction/binarySingleNaN.ml
-extraction/binary.ml
-extraction/binary.mli
 extraction/binInt.ml
 extraction/binInt.mli
-extraction/binNatDef.ml
-extraction/binNatDef.mli
 extraction/binNat.ml
 extraction/binNat.mli
+extraction/binNatDef.ml
+extraction/binNatDef.mli
 extraction/binNums.ml
 extraction/binNums.mli
-extraction/binPosDef.ml
-extraction/binPosDef.mli
 extraction/binPos.ml
 extraction/binPos.mli
+extraction/binPosDef.ml
+extraction/binPosDef.mli
+extraction/binary.ml
+extraction/binary.mli
+extraction/binarySingleNaN.ml
+extraction/binarySingleNaN.mli
 extraction/bits.ml
 extraction/bits.mli
 extraction/bool.ml
 extraction/bool.mli
-extraction/byte.mli
 extraction/byte.ml
-extraction/byte0.mli
+extraction/byte.mli
 extraction/byte0.ml
-extraction/byteCompare.mli
+extraction/byte0.mli
 extraction/byteCompare.ml
-extraction/bytestring.mli
+extraction/byteCompare.mli
 extraction/bytestring.ml
+extraction/bytestring.mli
+extraction/cRelationClasses.ml
+extraction/cRelationClasses.mli
 extraction/classes1.ml
 extraction/classes1.mli
 extraction/classes2.ml
 extraction/classes2.mli
-extraction/ctypesdefs.mli
-extraction/ctypesdefs.ml
 extraction/clight.ml
 extraction/clight.mli
 extraction/closure_conversion.ml
 extraction/closure_conversion.mli
-extraction/compile0.ml
-extraction/compile0.mli
-# extraction/compile1.ml
-# extraction/compile1.mli
 extraction/compM.ml
 extraction/compM.mli
+extraction/compile0.ml
+extraction/compile0.mli
 extraction/config0.ml
 extraction/config0.mli
 extraction/cop.ml
@@ -128,138 +100,126 @@ extraction/coqlib0.ml
 extraction/coqlib0.mli
 extraction/cps.ml
 extraction/cps.mli
-extraction/cps_proto_univ.mli
-extraction/cps_proto_univ.ml
 extraction/cps_proto.ml
 extraction/cps_proto.mli
+extraction/cps_proto_univ.ml
+extraction/cps_proto_univ.mli
 extraction/cps_show.ml
 extraction/cps_show.mli
 extraction/cps_util.ml
 extraction/cps_util.mli
 extraction/csyntax.ml
 extraction/csyntax.mli
-extraction/primInt63.mli
-extraction/primInt63.ml
-extraction/uint0.mli
-extraction/uint0.ml
-extraction/show.mli
-extraction/show.ml
-# extraction/decimalString.mli
-# extraction/decimalString.ml
-# extraction/hexadecimalString.mli
-# extraction/hexadecimalString.ml
-extraction/primitive.mli
-extraction/primitive.ml
-extraction/pCUICPrimitive.mli
-extraction/pCUICPrimitive.ml
 extraction/ctx.ml
 extraction/ctx.mli
 extraction/ctypes.ml
 extraction/ctypes.mli
+extraction/ctypesdefs.ml
+extraction/ctypesdefs.mli
 extraction/datatypes.ml
 extraction/datatypes.mli
 extraction/dead_param_elim.ml
 extraction/dead_param_elim.mli
+extraction/decidableClass.ml
+extraction/decidableClass.mli
+extraction/decidableType.ml
+extraction/decidableType.mli
 extraction/decimal.ml
 extraction/decimal.mli
-extraction/transform.mli
-extraction/transform.ml
-extraction/ePrimitive.mli
-extraction/ePrimitive.ml
 extraction/eAst.ml
 extraction/eAst.mli
-extraction/eGlobalEnv.mli
-extraction/eGlobalEnv.ml
 extraction/eAstUtils.ml
 extraction/eAstUtils.mli
-extraction/eEnvMap.mli
+extraction/eBeta.ml
+extraction/eBeta.mli
+extraction/eCSubst.ml
+extraction/eCSubst.mli
+extraction/eCoInductiveToInductive.ml
+extraction/eCoInductiveToInductive.mli
+extraction/eConstructorsAsBlocks.ml
+extraction/eConstructorsAsBlocks.mli
 extraction/eEnvMap.ml
+extraction/eEnvMap.mli
+extraction/eEtaExpanded.ml
+extraction/eEtaExpanded.mli
+extraction/eGlobalEnv.ml
+extraction/eGlobalEnv.mli
+extraction/eInduction.ml
+extraction/eInduction.mli
+extraction/eInlineProjections.ml
+extraction/eInlineProjections.mli
+extraction/eInlining.ml
+extraction/eInlining.mli
 extraction/eLiftSubst.ml
 extraction/eLiftSubst.mli
-extraction/ePretty.mli
-extraction/ePretty.ml
-extraction/resultMonad.mli
-extraction/resultMonad.ml
-extraction/exAst.mli
-extraction/exAst.ml
-extraction/fin.mli
-extraction/fin.ml
-extraction/vectorDef.mli
-extraction/vectorDef.ml
-extraction/vector.mli
-extraction/vector.ml
-extraction/optimize.mli
-extraction/optimize.ml
-extraction/optimizeCorrectness.mli
-extraction/optimizeCorrectness.ml
-extraction/eCSubst.ml
-extraction/eCSubst.mli
-extraction/eWellformed.mli
-extraction/eWellformed.ml
-extraction/eProgram.mli
-extraction/eProgram.ml
-extraction/eWcbvEval.mli
-extraction/eWcbvEval.ml
-extraction/environment.ml
-extraction/environment.mli
 extraction/eOptimizePropDiscr.ml
 extraction/eOptimizePropDiscr.mli
-extraction/eInduction.ml
-extraction/eInduction.mli
-extraction/eSpineView.ml
-extraction/eSpineView.mli
-extraction/eEtaExpanded.ml
-extraction/eEtaExpanded.mli
+extraction/ePretty.ml
+extraction/ePretty.mli
+extraction/ePrimitive.ml
+extraction/ePrimitive.mli
+extraction/eProgram.ml
+extraction/eProgram.mli
 extraction/eRemoveParams.ml
 extraction/eRemoveParams.mli
-extraction/eInlineProjections.mli
-extraction/eInlineProjections.ml
-extraction/eConstructorsAsBlocks.mli
-extraction/eConstructorsAsBlocks.ml
-extraction/eUnboxing.mli
-extraction/eUnboxing.ml
-extraction/eInlining.mli
-extraction/eInlining.ml
-extraction/eBeta.mli
-extraction/eBeta.ml
-extraction/eCoInductiveToInductive.mli
-extraction/eCoInductiveToInductive.ml
-extraction/eReorderCstrs.mli
 extraction/eReorderCstrs.ml
-extraction/eTransform.mli
+extraction/eReorderCstrs.mli
+extraction/eSpineView.ml
+extraction/eSpineView.mli
 extraction/eTransform.ml
+extraction/eTransform.mli
+extraction/eUnboxing.ml
+extraction/eUnboxing.mli
+extraction/eWcbvEval.ml
+extraction/eWcbvEval.mli
+extraction/eWellformed.ml
+extraction/eWellformed.mli
+extraction/envMap.ml
+extraction/envMap.mli
+extraction/environment.ml
+extraction/environment.mli
+extraction/environmentTyping.ml
+extraction/environmentTyping.mli
 extraction/eqDecInstances.ml
 extraction/eqDecInstances.mli
 extraction/equalities.ml
 extraction/equalities.mli
+extraction/erasure.ml
+extraction/erasure.mli
+extraction/erasure0.ml
+extraction/erasure0.mli
 extraction/erasureFunction.ml
 extraction/erasureFunction.mli
-extraction/erasureFunctionProperties.mli
 extraction/erasureFunctionProperties.ml
-extraction/optimizePropDiscr.mli
-extraction/optimizePropDiscr.ml
-extraction/extractionCorrectness.mli
-extraction/extractionCorrectness.ml
-extraction/erasure0.mli
-extraction/erasure0.ml
-extraction/erasure.ml
-extraction/erasure.mli
+extraction/erasureFunctionProperties.mli
 extraction/errors0.ml
 extraction/errors0.mli
-extraction/cRelationClasses.mli
-extraction/cRelationClasses.ml
-# extraction/eGlobalEnv.ml
-# extraction/eGlobalEnv.mli
+extraction/etaExpand.ml
+extraction/etaExpand.mli
 extraction/eval.ml
 extraction/eval.mli
+extraction/exAst.ml
+extraction/exAst.mli
 extraction/exceptionMonad.ml
 extraction/exceptionMonad.mli
 extraction/expression.ml
 extraction/expression.mli
 extraction/extract.ml
 extraction/extract.mli
+extraction/extractionCorrectness.ml
+extraction/extractionCorrectness.mli
+extraction/fMapAVL.ml
+extraction/fMapAVL.mli
+extraction/fMapFacts.ml
+extraction/fMapFacts.mli
+extraction/fMapInterface.ml
+extraction/fMapInterface.mli
+extraction/fMapList.ml
+extraction/fMapList.mli
 extraction/ffi.ml
 extraction/ffi.mli
+extraction/fin.ml
+extraction/fin.mli
 extraction/floatOps.ml
 extraction/floatOps.mli
 extraction/floats.ml
@@ -276,32 +236,30 @@ extraction/hexadecimal.ml
 extraction/hexadecimal.mli
 extraction/hoisting.ml
 extraction/hoisting.mli
-extraction/identifiers.ml
-extraction/identifiers.mli
 extraction/iEEE754_extra.ml
 extraction/iEEE754_extra.mli
-extraction/int0.mli
-extraction/int0.ml
+extraction/identifiers.ml
+extraction/identifiers.mli
 extraction/init.ml
 extraction/init.mli
-extraction/inline_letapp.ml
-extraction/inline_letapp.mli
 extraction/inline.ml
 extraction/inline.mli
+extraction/inline_letapp.ml
+extraction/inline_letapp.mli
+extraction/int0.ml
+extraction/int0.mli
 extraction/integers.ml
 extraction/integers.mli
 extraction/kernames.ml
 extraction/kernames.mli
-extraction/lambdaBoxMut_to_LambdaBoxLocal.ml
-extraction/lambdaBoxMut_to_LambdaBoxLocal.mli
-extraction/lambdaBoxLocal_to_LambdaANF.ml
-extraction/lambdaBoxLocal_to_LambdaANF.mli
-extraction/optionMonad.mli
-extraction/optionMonad.ml
 extraction/lambdaANF_to_Clight.ml
 extraction/lambdaANF_to_Clight.mli
 extraction/lambdaANF_to_Clight_stack.ml
 extraction/lambdaANF_to_Clight_stack.mli
+extraction/lambdaBoxLocal_to_LambdaANF.ml
+extraction/lambdaBoxLocal_to_LambdaANF.mli
+extraction/lambdaBoxMut_to_LambdaBoxLocal.ml
+extraction/lambdaBoxMut_to_LambdaBoxLocal.mli
 extraction/lambda_lifting.ml
 extraction/lambda_lifting.mli
 extraction/list0.ml
@@ -310,48 +268,22 @@ extraction/list_util.ml
 extraction/list_util.mli
 extraction/logic0.ml
 extraction/logic0.mli
-extraction/maps.ml
-extraction/maps.mli
-extraction/utils.mli
-extraction/utils.ml
-extraction/maps_util.ml
-extraction/maps_util.mli
-extraction/map_util.ml
-extraction/map_util.mli
-#extraction/decimalString.mli
-#extraction/decimalString.ml
-extraction/reflectEq.mli
-extraction/reflectEq.ml
-extraction/mCString.mli
-extraction/mCString.ml
 extraction/mCCompare.ml
 extraction/mCCompare.mli
 extraction/mCList.ml
 extraction/mCList.mli
-extraction/mCReflect.ml
-extraction/mCReflect.mli
 extraction/mCOption.ml
 extraction/mCOption.mli
 extraction/mCPrelude.ml
 extraction/mCPrelude.mli
 extraction/mCProd.ml
 extraction/mCProd.mli
-extraction/reflect.mli
-extraction/reflect.ml
-extraction/memdata.ml
-extraction/memdata.mli
-extraction/memory.ml
-extraction/memory.mli
-extraction/memtype.ml
-extraction/memtype.mli
-extraction/monad0.ml
-extraction/monad0.mli
-# extraction/monadExc.ml
-# extraction/monadExc.mli
-extraction/monadState.ml
-extraction/monadState.mli
-extraction/monad_utils.ml
-extraction/monad_utils.mli
+extraction/mCReflect.ml
+extraction/mCReflect.mli
+extraction/mCString.ml
+extraction/mCString.mli
+extraction/mSetAVL.ml
+extraction/mSetAVL.mli
 extraction/mSetDecide.ml
 extraction/mSetDecide.mli
 extraction/mSetFacts.ml
@@ -360,28 +292,52 @@ extraction/mSetInterface.ml
 extraction/mSetInterface.mli
 extraction/mSetList.ml
 extraction/mSetList.mli
-extraction/mSetAVL.mli
-extraction/mSetAVL.ml
 extraction/mSetProperties.ml
 extraction/mSetProperties.mli
 extraction/mSetRBT.ml
 extraction/mSetRBT.mli
+extraction/map_util.ml
+extraction/map_util.mli
+extraction/maps.ml
+extraction/maps.mli
+extraction/maps_util.ml
+extraction/maps_util.mli
+extraction/memdata.ml
+extraction/memdata.mli
+extraction/memory.ml
+extraction/memory.mli
+extraction/memtype.ml
+extraction/memtype.mli
+extraction/monad0.ml
+extraction/monad0.mli
+extraction/monadState.ml
+extraction/monadState.mli
+extraction/monad_utils.ml
+extraction/monad_utils.mli
 extraction/nat0.ml
 extraction/nat0.mli
 extraction/number0.ml
 extraction/number0.mli
+extraction/optimize.ml
+extraction/optimize.mli
+extraction/optimizeCorrectness.ml
+extraction/optimizeCorrectness.mli
+extraction/optimizePropDiscr.ml
+extraction/optimizePropDiscr.mli
+extraction/optionMonad.ml
+extraction/optionMonad.mli
 extraction/orderedType0.ml
 extraction/orderedType0.mli
 extraction/orderedTypeAlt.ml
 extraction/orderedTypeAlt.mli
+extraction/orders.ml
+extraction/orders.mli
 extraction/ordersEx.ml
 extraction/ordersEx.mli
 extraction/ordersFacts.ml
 extraction/ordersFacts.mli
 extraction/ordersLists.ml
 extraction/ordersLists.mli
-extraction/orders.ml
-extraction/orders.mli
 extraction/ordersTac.ml
 extraction/ordersTac.mli
 extraction/pCUICAst.ml
@@ -390,57 +346,68 @@ extraction/pCUICAstUtils.ml
 extraction/pCUICAstUtils.mli
 extraction/pCUICCases.ml
 extraction/pCUICCases.mli
+extraction/pCUICEqualityDec.ml
+extraction/pCUICEqualityDec.mli
 extraction/pCUICErrors.ml
 extraction/pCUICErrors.mli
 extraction/pCUICExpandLets.ml
 extraction/pCUICExpandLets.mli
-extraction/pCUICEqualityDec.mli
-extraction/pCUICEqualityDec.ml
 extraction/pCUICNormal.ml
 extraction/pCUICNormal.mli
 extraction/pCUICPosition.ml
 extraction/pCUICPosition.mli
-# extraction/pCUICPrimitive.ml
-# extraction/pCUICPrimitive.mli
+extraction/pCUICPrimitive.ml
+extraction/pCUICPrimitive.mli
+extraction/pCUICProgram.ml
+extraction/pCUICProgram.mli
 extraction/pCUICSafeReduce.ml
 extraction/pCUICSafeReduce.mli
 extraction/pCUICSafeRetyping.ml
 extraction/pCUICSafeRetyping.mli
+extraction/pCUICTransform.ml
+extraction/pCUICTransform.mli
 extraction/pCUICTyping.ml
 extraction/pCUICTyping.mli
-extraction/pCUICProgram.mli
-extraction/pCUICProgram.ml
-extraction/pCUICTransform.mli
-extraction/pCUICTransform.ml
-
+extraction/pCUICWfEnv.ml
+extraction/pCUICWfEnv.mli
+extraction/pCUICWfEnvImpl.ml
+extraction/pCUICWfEnvImpl.mli
+extraction/pOrderedType.ml
+extraction/pOrderedType.mli
 extraction/peanoNat.ml
 extraction/peanoNat.mli
 extraction/pipeline.ml
 extraction/pipeline.mli
 extraction/pipeline_utils.ml
 extraction/pipeline_utils.mli
-extraction/pOrderedType.ml
-extraction/pOrderedType.mli
 extraction/primFloat.ml
 extraction/primFloat.mli
-# extraction/primInt63.ml
-# extraction/primInt63.mli
-extraction/prototype.ml
-extraction/prototype.mli
+extraction/primInt63.ml
+extraction/primInt63.mli
+extraction/primitive.ml
+extraction/primitive.mli
 extraction/proto_util.ml
 extraction/proto_util.mli
+extraction/prototype.ml
+extraction/prototype.mli
 extraction/randyPrelude.ml
 extraction/randyPrelude.mli
+extraction/reflect.ml
+extraction/reflect.mli
+extraction/reflectEq.ml
+extraction/reflectEq.mli
 extraction/rename.ml
 extraction/rename.mli
+extraction/resultMonad.ml
+extraction/resultMonad.mli
 extraction/rewriting.ml
 extraction/rewriting.mli
 extraction/round.ml
 extraction/round.mli
-# extraction/safeTemplateChecker.ml
-# extraction/safeTemplateChecker.mli
 extraction/set_util.ml
 extraction/set_util.mli
+extraction/show.ml
+extraction/show.mli
 extraction/shrink_cps.ml
 extraction/shrink_cps.mli
 extraction/signature.ml
@@ -459,36 +426,46 @@ extraction/stateMonad.ml
 extraction/stateMonad.mli
 extraction/string0.ml
 extraction/string0.mli
-extraction/templateEnvMap.mli
 extraction/templateEnvMap.ml
+extraction/templateEnvMap.mli
 extraction/templateProgram.ml
 extraction/templateProgram.mli
 extraction/templateToPCUIC.ml
 extraction/templateToPCUIC.mli
+extraction/toplevel.ml
+extraction/toplevel.mli
 extraction/toplevel0.ml
 extraction/toplevel0.mli
 extraction/toplevel1.ml
 extraction/toplevel1.mli
 extraction/toplevel2.ml
 extraction/toplevel2.mli
-# extraction/topleveLambdaBoxMut.ml
-# extraction/topleveLambdaBoxMut.mli
-extraction/toplevel.ml
-extraction/toplevel.mli
+extraction/transform.ml
+extraction/transform.mli
+extraction/typing0.ml
+extraction/typing0.mli
 extraction/uGraph0.ml
 extraction/uGraph0.mli
-# extraction/uint0.ml
-# extraction/uint0.mli
+extraction/uint0.ml
+extraction/uint0.mli
 extraction/uncurry.ml
 extraction/uncurry.mli
 extraction/uncurry_proto.ml
 extraction/uncurry_proto.mli
 extraction/universes0.ml
 extraction/universes0.mli
+extraction/utils.ml
+extraction/utils.mli
 extraction/values0.ml
 extraction/values0.mli
+extraction/vector.ml
+extraction/vector.mli
+extraction/vectorDef.ml
+extraction/vectorDef.mli
 extraction/wGraph.ml
 extraction/wGraph.mli
+extraction/wf.ml
+extraction/wf.mli
 extraction/zArith_dec.ml
 extraction/zArith_dec.mli
 extraction/zbits.ml
diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml
index 02ba971e..5a700f29 100644
--- a/plugin/certicoq.ml
+++ b/plugin/certicoq.ml
@@ -11,17 +11,14 @@ open Plugin_utils
 
 let get_stringopt_option key =
   let open Goptions in
-  let tables = get_tables () in
-  try
-    let _ = OptionMap.find key tables in
-    fun () ->
-      let tables = get_tables () in
-      let opt = OptionMap.find key tables in
-      match opt.opt_value with
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
       | StringOptValue b -> b
       | _ -> assert false
-  with Not_found ->
-    declare_stringopt_option_and_ref ~depr:false ~key
+      end
+  | None ->
+    (declare_stringopt_option_and_ref ~key ~value:None ()).get
 
 let get_build_dir_opt =
   get_stringopt_option ["CertiCoq"; "Build"; "Directory"]
@@ -373,6 +370,53 @@ module CompileFunctor (CI : CompilerInterface) = struct
   let make_fname opts str =
     Filename.concat opts.build_dir str
 
+  type line = 
+  | EOF
+  | Info of string
+  | Error of string
+  
+  let read_line stdout stderr =
+    try Info (input_line stdout)
+    with End_of_file -> 
+      try Error (input_line stderr)
+    with End_of_file -> EOF
+  
+  let push_line buf line =
+    Buffer.add_string buf line; 
+    Buffer.add_string buf "\n"
+  
+  let string_of_buffer buf = Bytes.to_string (Buffer.to_bytes buf)
+    
+  let execute cmd =
+    debug Pp.(fun () -> str "Executing: " ++ str cmd ++ str " in environemt: " ++ 
+      prlist_with_sep spc str (Array.to_list (Unix.environment ())));
+    let (stdout, stdin, stderr) = Unix.open_process_full cmd (Unix.environment ()) in
+    let continue = ref true in
+    let outbuf, errbuf = Buffer.create 100, Buffer.create 100 in
+    let push_info = push_line outbuf in
+    let push_error = push_line errbuf in
+    while !continue do
+      match read_line stdout stderr with
+      | EOF -> debug Pp.(fun () -> str "Program terminated"); continue := false
+      | Info s -> push_info s
+      | Error s -> push_error s
+    done;
+    let status = Unix.close_process_full (stdout, stdin, stderr) in
+    status, string_of_buffer outbuf, string_of_buffer errbuf
+    
+  let execute ?loc cmd =
+    let status, out, err = execute cmd in
+    match status with
+    | Unix.WEXITED 0 -> out, err
+    | Unix.WEXITED n -> 
+      CErrors.user_err ?loc Pp.(str"Command" ++ spc () ++ str cmd ++ spc () ++
+        str"exited with code " ++ int n ++ str "." ++ fnl () ++
+        str"stdout: " ++ spc () ++ str out ++ fnl () ++ str "stderr: " ++ str err)
+    | Unix.WSIGNALED n | Unix.WSTOPPED n -> 
+      CErrors.user_err ?loc Pp.(str"Command" ++ spc () ++ str cmd ++ spc () ++ 
+      str"was signaled with code " ++ int n ++ str"." ++ fnl () ++
+      str"stdout: " ++ spc () ++ str out ++ fnl () ++ str "stderr: " ++ str err)
+    
   let compile opts term imports =
     let debug = opts.debug in
     let options = make_pipeline_options opts in
@@ -473,11 +517,6 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | None -> find_executable debug "which ocamlfind"
     | Some s -> s
       
-  type line = 
-    | EOF
-    | Info of string
-    | Error of string
-
   let read_line stdout stderr =
     try Info (input_line stdout)
     with End_of_file -> 
@@ -548,8 +587,8 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n  ++ str" while running " ++ str cmd)
     
   type reifyable_type =
-  | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list
-  | IsPrimitive of Names.Constant.t * Univ.Instance.t * Constr.t list
+  | IsInductive of Names.inductive * UVars.Instance.t * Constr.t list
+  | IsPrimitive of Names.Constant.t * UVars.Instance.t * Constr.t list
   
   let type_of_reifyable_type = function
     | IsInductive (hd, u, args) -> Term.applistc (Constr.mkIndU ((hd, u))) args
@@ -587,7 +626,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let hd, args = EConstr.decompose_app sigma hnf in
       match EConstr.kind sigma hd with
       | Const (c, u) when Environ.is_primitive_type env c -> 
-        IsPrimitive (c, EConstr.EInstance.kind sigma u, List.map EConstr.Unsafe.to_constr args)
+        IsPrimitive (c, EConstr.EInstance.kind sigma u, CArray.map_to_list EConstr.Unsafe.to_constr args)
       | _ -> CErrors.user_err 
         Pp.(str"Cannot reify values of non-inductive or non-primitive type: " ++ 
           Printer.pr_econstr_env env sigma ty)
@@ -743,32 +782,25 @@ module CompileFunctor (CI : CompilerInterface) = struct
       "coq-core.interp"; "coq-core.kernel"; "coq-core.library"] in
     let pkgs = String.concat "," packages in
     let dontlink = "str,unix,dynlink,threads,zarith,coq-core,coq-core.plugins.ltac,coq-core.interp" in
-    match Unix.system cmd with
-    | Unix.WEXITED 0 ->
-      let shared_lib = make_fname opts opts.filename ^ suff ^ ".cmxs" in
-      let linkcmd =
-        Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \
-        -I %s -I plugin -o %s %s %s %s %s"
-        ocamlfind dontlink pkgs opts.build_dir shared_lib ocaml_driver gc_stack_o 
-        (make_fname opts opts.filename ^ ".o") importso
-      in
-      debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd);
-      (match Unix.system linkcmd with
-      | Unix.WEXITED 0 ->
-          debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" global_id);
-          Dynlink.loadfile_private shared_lib;
-          debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" global_id);
-          let result = 
-            if opts.time then time ~msg:(Pp.str id) (run_certicoq_run global_id)
-            else run_certicoq_run global_id ()
-          in
-          debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result");
-          reify opts env sigma tyinfo result
-      | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str linkcmd)
-      | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n))
-    | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str cmd)
-    | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n  ++ str" while running " ++ str cmd)
-
+    let () = ignore (execute cmd) in
+    let shared_lib = make_fname opts opts.filename ^ suff ^ ".cmxs" in
+    let linkcmd =
+      Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \
+      -I %s -I plugin -o %s %s %s %s %s"
+      ocamlfind dontlink pkgs opts.build_dir shared_lib ocaml_driver gc_stack_o 
+      (make_fname opts opts.filename ^ ".o") importso
+    in
+    debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd);
+    let _out, _err = execute linkcmd in
+    Dynlink.loadfile_private shared_lib;
+    debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" global_id);
+    let result = 
+      if opts.time then time ~msg:(Pp.str id) (run_certicoq_run global_id)
+      else run_certicoq_run global_id ()
+    in
+    debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result");
+    reify opts env sigma tyinfo result
+    
   let next_string_away_from s bad =
     let rec name_rec s = if bad s then name_rec (increment_subscript s) else s in
     name_rec s
diff --git a/plugin/certicoq_plugin.mlpack b/plugin/certicoq_plugin.mlpack
index eec0ffb0..4965722f 100644
--- a/plugin/certicoq_plugin.mlpack
+++ b/plugin/certicoq_plugin.mlpack
@@ -4,11 +4,13 @@ Tm_util
 
 Datatypes
 Caml_nat
+DecidableClass
 Bool
 Equalities
 Decimal
 Hexadecimal
 Nat0
+Wf
 List0
 PeanoNat
 Specif
diff --git a/plugin/g_certicoq.mlg b/plugin/g_certicoq.mlg
index 7c3d31ce..5fbea6c3 100644
--- a/plugin/g_certicoq.mlg
+++ b/plugin/g_certicoq.mlg
@@ -86,8 +86,8 @@ END
 
 VERNAC ARGUMENT EXTEND cinclude
 | [ string(str) ] -> { FromRelativePath str }
-| [ string(str) "as" "absolute" ] -> { FromAbsolutePath str }
-| [ string(str) string_opt(str') "as" "library" ] -> { FromLibrary (str, str') }
+| [ "Library" string(str) string_opt(str') ] -> { FromLibrary (str, str') }
+| [ "Absolute" string(str) ] -> { FromAbsolutePath str }
 END
 
 VERNAC COMMAND EXTEND CertiCoq_Register CLASSIFIED AS SIDEFF
diff --git a/plugin/plugin_utils.ml b/plugin/plugin_utils.ml
index f2e8008b..067234fc 100644
--- a/plugin/plugin_utils.ml
+++ b/plugin/plugin_utils.ml
@@ -3,26 +3,24 @@ open Names
 open Pp
 open Caml_bytestring
 
+  
 let debug_opt =
-   let open Goptions in
-   let key = ["CertiCoq"; "Debug"] in
-   let tables = get_tables () in
-   try
-     let _ = OptionMap.find key tables in
-     fun () ->
-       let tables = get_tables () in
-       let opt = OptionMap.find key tables in
-       match opt.opt_value with
-       | BoolValue b -> b
-       | _ -> assert false
-   with Not_found ->
-   declare_bool_option_and_ref ~depr:false ~key ~value:false
- 
- let debug (m : unit ->Pp.t) =
-   if debug_opt () then
-     Feedback.(msg_debug (m ()))
-   else
-     ()
+  let open Goptions in
+  let key = ["CertiCoq"; "Debug"] in
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
+      | BoolValue b -> b
+      | _ -> assert false
+      end
+  | None ->
+   (declare_bool_option_and_ref ~key ~value:false ()).get
+
+let debug (m : unit ->Pp.t) =
+  if debug_opt () then
+    Feedback.(msg_debug (m ()))
+  else
+    ()
 
 type import =
     FromRelativePath of string
@@ -76,7 +74,7 @@ Valid options:\n\
 -fast-erasure     :  Uses an alternative function to remove parameters of constructors in the MetaCoq Erasure pipeline.\n\
 \n\n\
 To compile Gallina constants to specific C functions use:\n\
-   CertiCoq Compile <options> <gid> Extract Constants [ constant1 => \"c_function1\", ... , constantN => \"c_functionN\" ] Include [ \"file1.h\" as library, ... , \"fileM.h\" as library ].\n\
+   CertiCoq Compile <options> <gid> Extract Constants [ constant1 => \"c_function1\", ... , constantN => \"c_functionN\" ] Include [ \"file1.h\" , Library \"runtime_header.h\", ... , Absolute \"fileM.h\" ].\n\
 \n\
 See https://github.com/CertiCoq/certicoq/wiki/The-CertiCoq-plugin for more detailed information."
 
diff --git a/plugin/runtime/gc_stack.c b/plugin/runtime/gc_stack.c
index f380cf1e..0ef06be3 100644
--- a/plugin/runtime/gc_stack.c
+++ b/plugin/runtime/gc_stack.c
@@ -207,6 +207,7 @@ void forward (value *from_start,  /* beginning of from-space */
         /* printf("New %lld\n", newv); */
         /* if (*p == 73832) printf("Found it\n"); */
         if (depth>0)
+	  if (!No_scan(Tag_hd(hd)))
           for (i=0; i<sz; i++)
             forward(from_start, from_limit, next, &Field(newv,i), depth-1);
       }
@@ -227,7 +228,7 @@ void forward_remset (struct space *from,  /* descriptor of from-space */
       forward(from_start, from_limit, next, p, DEPTH);
       newp= *p;
       if (oldp!=newp)
-          *(--to->limit) = (value)q;
+          *(--to->limit) = (value)p;
     }
     q++;
   }
diff --git a/plugin/tm_util.ml b/plugin/tm_util.ml
index 8be3e3c9..235e5b74 100644
--- a/plugin/tm_util.ml
+++ b/plugin/tm_util.ml
@@ -4,20 +4,17 @@ let contrib_name = "template-coq"
 
 (* This allows to load template_plugin and the extractable plugin at the same time 
   while have option settings apply to both *)
-  let timing_opt =
+let timing_opt =
   let open Goptions in
   let key = ["MetaCoq"; "Timing"] in
-  let tables = get_tables () in
-  try 
-    let _ = OptionMap.find key tables in
-    fun () -> 
-      let tables = get_tables () in
-      let opt = OptionMap.find key tables in
-      match opt.opt_value with
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
       | BoolValue b -> b
       | _ -> assert false
-  with Not_found ->
-    declare_bool_option_and_ref ~depr:false ~key ~value:false
+      end
+  | None ->
+    (declare_bool_option_and_ref ~key ~value:false ()).get
 
 let time prefix f x =
   if timing_opt () then 
@@ -31,17 +28,14 @@ let time prefix f x =
 let debug_opt =
   let open Goptions in
   let key = ["MetaCoq"; "Debug"] in
-  let tables = get_tables () in
-  try 
-    let _ = OptionMap.find key tables in
-    fun () -> 
-      let tables = get_tables () in
-      let opt = OptionMap.find key tables in
-      match opt.opt_value with
+  match get_option_value key with
+  | Some get -> fun () ->
+      begin match get () with
       | BoolValue b -> b
       | _ -> assert false
-  with Not_found ->
-  declare_bool_option_and_ref ~depr:false ~key ~value:false
+      end
+  | None ->
+   (declare_bool_option_and_ref ~key ~value:false ()).get
 
 let debug (m : unit ->Pp.t) =
   if debug_opt () then
@@ -134,15 +128,15 @@ module CaseCompat =
     in
     instantiate (Array.length nas - 1) ctx
 
-  let case_predicate_context_gen mip ci u paramsubst nas =
-    let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
-    let self =
-      let args = Context.Rel.to_extended_vect mkRel 0 mip.mind_arity_ctxt in
-      let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in
-      mkApp (mkIndU (ci.ci_ind, inst), args)
-    in
-    let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
-    instantiate_context u paramsubst nas realdecls
+    let case_predicate_context_gen mip ci u paramsubst nas =
+      let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+      let self =
+        let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
+        let inst = UVars.Instance.abstract_instance (UVars.Instance.length u) in
+        mkApp (mkIndU (ci.ci_ind, inst), args)
+      in
+      let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
+      instantiate_context u paramsubst nas realdecls
 
   let case_predicate_context env ci u params nas =
     let mib = Environ.lookup_mind (fst ci.ci_ind) env in
diff --git a/submodules/metacoq b/submodules/metacoq
index 60374183..9af0b0fc 160000
--- a/submodules/metacoq
+++ b/submodules/metacoq
@@ -1 +1 @@
-Subproject commit 603741834df00f3dff90c308218eeeb044c241f8
+Subproject commit 9af0b0fc7b8c3a2989aae8a11e6a6b24695128ef
diff --git a/theories/Extraction/extraction.v b/theories/Extraction/extraction.v
index 3f885b69..377fbd41 100644
--- a/theories/Extraction/extraction.v
+++ b/theories/Extraction/extraction.v
@@ -9,7 +9,7 @@ Require compcert.common.AST
         compcert.lib.Coqlib
         compcert.lib.Floats
         compcert.common.Globalenvs
-        Int31.
+       (* Int63*).
 
 Require Glue.glue
         Compiler.pipeline.
@@ -81,6 +81,8 @@ Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false".
 Set Warnings "-extraction-reserved-identifier".
 Set Warnings "-extraction-opaque-accessed".
 
+Set Extraction Output Directory ".".
+
 Extraction Library Zeven.
 Extraction Library Zeven.
 Extraction Library ZArith_dec.
diff --git a/theories/ExtractionVanilla/extraction.v b/theories/ExtractionVanilla/extraction.v
index a2ac40ee..e1efa6ec 100644
--- a/theories/ExtractionVanilla/extraction.v
+++ b/theories/ExtractionVanilla/extraction.v
@@ -9,7 +9,7 @@ Require compcert.common.AST
         compcert.lib.Coqlib
         compcert.lib.Floats
         compcert.common.Globalenvs
-        Int31.
+    (*    Int31*).
 
 Require Glue.glue
         Compiler.pipeline.
@@ -94,6 +94,8 @@ Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false".
 Set Warnings "-extraction-reserved-identifier".
 Set Warnings "-extraction-opaque-accessed".
 
+Set Extraction Output Directory ".".
+
 Extraction Library Zeven.
 Extraction Library Zeven.
 Extraction Library ZArith_dec.
diff --git a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v
index 2f7a68b0..3d2d5fbb 100644
--- a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v
+++ b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v
@@ -2180,8 +2180,8 @@ Section Correct.
                     eapply H1 in H16. eapply HS2 in H16. inv_setminus. eapply Hdis; eauto.
                   - eapply Forall2_app.
                     rewrite <- rev_involutive with (l := x2). eapply All_Forall.Forall2_rev.
-                    rewrite app_nil_end with (l := vs').
-                    rewrite app_nil_end with (l := rev x2).
+                    rewrite <- app_nil_r with (l := vs').
+                    rewrite <- app_nil_r with (l := rev x2).
                     eapply cps_env_rel_extend_setlists. now constructor.
                     eapply get_list_set_lists.
                     now eapply NoDup_rev; eauto.
@@ -2250,8 +2250,8 @@ Section Correct.
             eapply H1 in H16. eapply HS2 in H16. inv_setminus. eapply Hdis; eauto.
           - eapply Forall2_app.
             rewrite <- rev_involutive with (l := x2). eapply All_Forall.Forall2_rev.
-            rewrite app_nil_end with (l := vs').
-            rewrite app_nil_end with (l := rev x2).
+            rewrite <- app_nil_r with (l := vs').
+            rewrite <- app_nil_r with (l := rev x2).
             eapply cps_env_rel_extend_setlists. now constructor.
             eapply get_list_set_lists.
             now eapply NoDup_rev; eauto.
diff --git a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v
index 3861fb88..098f5653 100644
--- a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v
+++ b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v
@@ -1457,7 +1457,7 @@ Section Post.
                Hm He1 He2 Hdup1 Hdup2 Hdup3 Hdup4 Hnd5 Hnot Hdis Hlen Hlen' Hlen''
                Hdis1 Hdis2 Hdis3 Hdis4 Hdis5 Hdis6 Hhyp Henv.
         inv He1; inv He2.
-        eapply Hhyp. rewrite <- !app_nil_end.
+        eapply Hhyp. rewrite !app_nil_r.
         eapply preord_env_P_inj_f_eq_subdomain.
         eapply preord_env_P_inj_antimon. eassumption.
         now sets.
diff --git a/theories/LambdaANF/bounds.v b/theories/LambdaANF/bounds.v
index d6bb32ed..ecc2e5c0 100644
--- a/theories/LambdaANF/bounds.v
+++ b/theories/LambdaANF/bounds.v
@@ -106,7 +106,7 @@ Section Bounds.
 
       - intro; intros. intro; intros. 
         unfold inline_bound in *; unfold_all; simpl.
-        assert (c = 0). eapply NPeano.Nat.lt_1_r. eassumption. subst. lia.
+        assert (c = 0). eapply Nat.lt_1_r. eassumption. subst. lia.
       - intro; intros. unfold post_base'. 
         unfold inline_bound in *; unfold_all; simpl. lia.
       - intro; intros; unfold inline_bound in *.
@@ -158,7 +158,7 @@ Section Bounds.
       
       assert (Hleq'' : cin1 <= cin2).
       { eapply Nat.add_le_mono_r in Hleq'. eapply Nat.add_le_mono_r in Hleq'.
-        eapply NPeano.Nat.mul_le_mono_pos_l in Hleq'. eassumption. lia. }
+        eapply Nat.mul_le_mono_pos_l in Hleq'. eassumption. lia. }
 
       eexists (cin2 - cin1). simpl. lia.
     Qed.
@@ -400,7 +400,7 @@ Section Bounds.
       eapply Nat.add_le_mono_r in H.
       replace (cin2 + G * cin2) with ((1 + G) * cin2) in H by lia.
       replace (G * cin1 + cin1) with ((1 + G) * cin1) in H by lia.      
-      eapply NPeano.Nat.mul_le_mono_pos_l in H.
+      eapply Nat.mul_le_mono_pos_l in H.
       eexists (cin2 - cin1). simpl. lia.
       lia.
     Qed.
diff --git a/theories/LambdaANF/closure_conversion_correct.v b/theories/LambdaANF/closure_conversion_correct.v
index c8ed61d8..d95c7784 100644
--- a/theories/LambdaANF/closure_conversion_correct.v
+++ b/theories/LambdaANF/closure_conversion_correct.v
@@ -565,7 +565,7 @@ Section Closure_conversion_correct.
     n <= n * m.
   Proof.
     rewrite Nat.mul_comm.
-    edestruct Arith_prebase.mult_O_le_stt; eauto. lia.
+    edestruct Arith_base.mult_O_le_stt; eauto. lia.
   Qed.
 
   Lemma plus_le_mult  (a1 a2 b1 b2 b3 : nat) :
@@ -575,7 +575,7 @@ Section Closure_conversion_correct.
     a1 + a2 <= (1 + b1) * a1 * b2.
   Proof.
     intros.
-    rewrite <- Nat.mul_assoc, NPeano.Nat.mul_add_distr_r.
+    rewrite <- Nat.mul_assoc, Nat.mul_add_distr_r.
     eapply Nat.add_le_mono.
     - simpl. rewrite <- plus_n_O.
       now eapply mult_le_n.
diff --git a/theories/LambdaANF/inline.v b/theories/LambdaANF/inline.v
index fa95223a..30a1ef81 100644
--- a/theories/LambdaANF/inline.v
+++ b/theories/LambdaANF/inline.v
@@ -81,7 +81,7 @@ Section Inline.
   Lemma split_fuel_add d :
     d = fst (split_fuel d) + snd (split_fuel d). 
   Proof.
-    unfold split_fuel. simpl. rewrite (NPeano.Nat.div2_odd d) at 1. simpl.    
+    unfold split_fuel. simpl. rewrite (Nat.div2_odd d) at 1. simpl.    
     lia.
   Qed.    
   
diff --git a/theories/LambdaANF/inline_correct.v b/theories/LambdaANF/inline_correct.v
index 7914c88c..4b1dcf8b 100644
--- a/theories/LambdaANF/inline_correct.v
+++ b/theories/LambdaANF/inline_correct.v
@@ -1582,7 +1582,7 @@ Section Inline_correct.
             - do 2 eapply frame_rule. eapply pre_transfer_r. eapply IHd.
               + lia.
               + eapply Nat.le_trans. reflexivity.
-                eapply NPeano.Nat.div2_decr. lia.
+                eapply Nat.div2_decr. lia.
               + eassumption.
               + eapply Union_Disjoint_r. clear H3. now sets. now sets.
               + repeat normalize_bound_var_in_ctx. repeat normalize_occurs_free_in_ctx.
diff --git a/theories/LambdaANF/lambda_lifting_correct.v b/theories/LambdaANF/lambda_lifting_correct.v
index f5dbae65..dea89178 100644
--- a/theories/LambdaANF/lambda_lifting_correct.v
+++ b/theories/LambdaANF/lambda_lifting_correct.v
@@ -1727,8 +1727,7 @@ Section Lambda_lifting_correct.
        unfold fun_map, lifted_name in *. rewrite M.gempty in H. congruence. }
 
      assert (Heq'' : Funs (fun_map (M.empty FunInfo)) <--> Empty_set _).
-     { clear. split; sets. intros x Hin. inv Hin. destructAll.
-       unfold fun_map, lifted_name in *. simpl in *. congruence. }
+     { clear. split; sets. intros x Hin. inv Hin. inv H. }
      
      rewrite !Heq, !Heq' in *.
 
diff --git a/theories/LambdaANF/shrink_cps_corresp.v b/theories/LambdaANF/shrink_cps_corresp.v
index b65c1806..fa796e80 100644
--- a/theories/LambdaANF/shrink_cps_corresp.v
+++ b/theories/LambdaANF/shrink_cps_corresp.v
@@ -7515,7 +7515,7 @@ Section CONTRACT.
                 apply bound_stem_var. auto.
                 simpl. constructor. inv H18. }
         * (* size *)
-          eapply NPeano.Nat.lt_le_trans.
+          eapply Nat.lt_le_trans.
           apply constr_sub_size.
           lia.
           (* cmap_view *)
diff --git a/theories/LambdaANF/uncurry_rel.v b/theories/LambdaANF/uncurry_rel.v
index 7b058f69..dd4f2350 100644
--- a/theories/LambdaANF/uncurry_rel.v
+++ b/theories/LambdaANF/uncurry_rel.v
@@ -37,7 +37,7 @@ Section list_lemmas.
       simpl in H. remember (set_lists l l1 rho).
       destruct o; [|congruence].
       rewrite <- IHl with (rho := rho). now exists t. 
-    - (* :: <- *) destruct l1; [easy|]. simpl in H. apply NPeano.Nat.succ_inj in H.
+    - (* :: <- *) destruct l1; [easy|]. simpl in H. apply Nat.succ_inj in H.
       rewrite <- IHl with (rho := rho) in H. destruct H.
       simpl. rewrite <- H. now exists (M.set a a0 x).
   Qed.
diff --git a/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v b/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v
index 90da2327..28407722 100644
--- a/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v
+++ b/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v
@@ -1284,7 +1284,7 @@ Lemma LambdaBoxMutsbst_fix_preserves_lam dts nm bod :
 Proof.
   revert nm bod; induction (list_to_zero (dlength dts)); simpl; intros.
   reflexivity.
-  simpl. rewrite LambdaBoxMut.term.instantiate_TLambda. 
+ (* simpl. rewrite LambdaBoxMut.term.instantiate_TLambda. *)
   simpl. rewrite IHl. reflexivity.
 Qed.
 
@@ -1548,7 +1548,7 @@ Proof.
     + apply (IHbrs (n + 1) n0 Hnth). clear IHbrs.
       now cbn in findbr.
   - intros.
-    elimtype False.
+    exfalso.
     apply find_branch_map_branches_none in H.
     rewrite find_branch_trans in H; eauto.
     revert n H Hnth. generalize 0 at 2.
@@ -2447,9 +2447,9 @@ Proof with eauto.
          intros Hfs.
          apply WcbvEval_preserves_crctTerm in evfn; eauto.
          destruct (crctTerm_fix _ _ _ _ _ evfn eqt') as [[nm [bod ->]]| ->].         
-         { elimtype False. subst x.
+         { exfalso. subst x.
           rewrite LambdaBoxMutsbst_fix_preserves_lam /= subst_env_aux_lam in H4. inv H4. }
-        { elimtype False. subst x.
+        { exfalso. subst x.
           rewrite LambdaBoxMutsbst_fix_preserves_TProof /= subst_env_aux_prf in H4. inv H4. }
 
       * intros Hfs.
@@ -2459,7 +2459,7 @@ Proof with eauto.
         rewrite efnlst_length_trans. reflexivity.
         apply WcbvEval_preserves_crctTerm in evfn; eauto.
         destruct (crctTerm_fix _ _ _ _ _ evfn eqt') as [[nm [bod ->]]| ->].
-        { elimtype False. subst x.
+        { exfalso. subst x.
           rewrite LambdaBoxMutsbst_fix_preserves_lam /= subst_env_aux_lam in H5. inv H5. }
         cbn. rewrite subst_env_aux_prf /=.
         eapply eval_ProofApp_e; eauto.
diff --git a/theories/LambdaBoxLocal/expression.v b/theories/LambdaBoxLocal/expression.v
index 3c12cafd..62400f33 100644
--- a/theories/LambdaBoxLocal/expression.v
+++ b/theories/LambdaBoxLocal/expression.v
@@ -649,7 +649,7 @@ Qed.
 Declare Scope name.
 Bind Scope name with name.
 Delimit Scope name with name.
-Arguments nNamed i%bs.
+Arguments nNamed i%_bs.
 Definition nNameds (s : string) : name := nNamed s.
 
 Notation " [: x ] " := (cons (nNameds x) nil) : name.
@@ -658,8 +658,8 @@ Notation " '[:' x , y , .. , z ] " :=
 Local Open Scope name.
 
 Coercion nNameds : string >-> name.
-Arguments Lam_e n%bs _.
-Arguments eflcons n%bs _ _.
+Arguments Lam_e n%_bs _.
+Arguments eflcons n%_bs _ _.
 
 Example x1: exp := Lam_e "x" (Var_e 0).  (* identity *)
 Lemma Lx1: forall (e d:exp), eval e d -> eval (App_e x1 e) d.
diff --git a/theories/LambdaBoxMut/stripEvalCommute.v b/theories/LambdaBoxMut/stripEvalCommute.v
index 7179ca90..e0c1eb11 100644
--- a/theories/LambdaBoxMut/stripEvalCommute.v
+++ b/theories/LambdaBoxMut/stripEvalCommute.v
@@ -788,7 +788,7 @@ Proof.
     move/andP: H0 => [] /andP[] wfi wft wfl.
     set (brs' := map _ l). cbn in brs'.
     set (brs'0 := map _ l). simpl.
-    rewrite instantiate_TCase. rtoProp; intuition auto. f_equal; eauto.
+(*    rewrite instantiate_TCase. *) rtoProp; intuition auto. f_equal; eauto.
     clear -X wfl.
     { subst brs' brs'0. repeat toAll. induction wfl.
     - constructor.
@@ -796,7 +796,7 @@ Proof.
       f_equal; eauto. destruct p. rewrite List.rev_length. repeat eapply (e n).
       eapply wellformed_up; tea. lia. }
   - rewrite map_map_compose. set (mfix' := map _ m).
-    simpl. rewrite instantiate_TFix. f_equal.
+    simpl. (*rewrite instantiate_TFix. *) f_equal.
     clear -X H.
     move/andP: H => [] _ /andP[] _ H1. repeat toAll.
     rewrite -dlength_hom. 
diff --git a/theories/LambdaBoxMut/term.v b/theories/LambdaBoxMut/term.v
index 2168dbdf..67c947bd 100644
--- a/theories/LambdaBoxMut/term.v
+++ b/theories/LambdaBoxMut/term.v
@@ -2632,9 +2632,9 @@ Proof.
         rewrite k0. reflexivity.
       * assert (k0: S (Init.Nat.pred n) = n). lia.
         rewrite k0. reflexivity.
-    + rewrite (proj2 (NPeano.Nat.compare_gt_iff _ _)); try lia. cbn.
+    + rewrite (proj2 (Nat.compare_gt_iff _ _)); try lia. cbn.
       rewrite match_cn_Eq; try lia. reflexivity.
-    + rewrite (proj2 (NPeano.Nat.compare_gt_iff _ _)); try lia. cbn.
+    + rewrite (proj2 (Nat.compare_gt_iff _ _)); try lia. cbn.
       rewrite match_cn_Lt; try lia. reflexivity.
     + rewrite match_cn_Gt; try lia. cbn. rewrite match_cn_Gt; try lia.
       reflexivity.
@@ -2795,7 +2795,7 @@ Proof.
   try (solve [unfold instantiate; constructor]).
   - destruct (lt_eq_lt_dec n m) as [[h|h]|h]; unfold instantiate.
     + rewrite (proj1 (nat_compare_lt _ _) h). constructor.
-    + rewrite (proj2 (NPeano.Nat.compare_eq_iff _ _) h). assumption.
+    + rewrite (proj2 (Nat.compare_eq_iff _ _) h). assumption.
     + rewrite (proj1 (nat_compare_gt _ _) h). constructor.
   - cbn. constructor. apply H0. assumption.
   - change (WFapp (TLetIn nm (instantiate n dfn) (instantiate (S n) bod))).
diff --git a/theories/Runtime/gc_stack.c b/theories/Runtime/gc_stack.c
index f380cf1e..727455ba 100644
--- a/theories/Runtime/gc_stack.c
+++ b/theories/Runtime/gc_stack.c
@@ -227,7 +227,7 @@ void forward_remset (struct space *from,  /* descriptor of from-space */
       forward(from_start, from_limit, next, p, DEPTH);
       newp= *p;
       if (oldp!=newp)
-          *(--to->limit) = (value)q;
+          *(--to->limit) = (value)p;
     }
     q++;
   }
diff --git a/theories/common/AstCommon.v b/theories/common/AstCommon.v
index 032ae0e7..6b1a8924 100644
--- a/theories/common/AstCommon.v
+++ b/theories/common/AstCommon.v
@@ -18,7 +18,7 @@ Set Implicit Arguments.
 Ltac inv H := inversion H; subst; clear H.
 
 (** Fix arguments scope for [mkInd]. *)
-Arguments mkInd _%bs _%nat.
+Arguments mkInd _%_bs _%_nat.
 
 (** Use with caution, valid kernames from Coq cannot have an empty MPFile component. *)
 Definition kername_of_string (s : string) := (MPfile nil, s).
diff --git a/theories/common/RandyPrelude.v b/theories/common/RandyPrelude.v
index 5f5889ab..f9591fd6 100644
--- a/theories/common/RandyPrelude.v
+++ b/theories/common/RandyPrelude.v
@@ -13,7 +13,7 @@ Require Import Coq.Arith.Arith.
 Require Import Coq.micromega.Lia.
 Require Import Common.exceptionMonad.
 Require Import FunInd.
-Require Import Coq.Arith.Div2 Coq.Numbers.Natural.Peano.NPeano Coq.Program.Wf.
+Require Import (*Coq.Arith.Div2*) (*Coq.Numbers.Natural.Peano.NPeano*) Coq.Program.Wf.
 Require Import MetaCoq.Utils.bytestring.
 Local Open Scope bs_scope.
 Local Open Scope bool.
@@ -37,12 +37,12 @@ Program Fixpoint nat_to_string (n:nat) {measure n}: string :=
   (match n <? 10 as x return n <? 10 = x -> string with
      | true => fun _ => digit_to_string n
      | false => fun pf =>
-                  let m := NPeano.Nat.div n 10 in
+                  let m := Nat.div n 10 in
                   (nat_to_string m) ++ (digit_to_string (n - 10 * m))
    end eq_refl)%nat.
 Next Obligation.
-  apply (NPeano.Nat.div_lt n 10%nat).
-  destruct n. unfold NPeano.Nat.ltb in *. simpl in *.
+  apply (Nat.div_lt n 10%nat).
+  destruct n. unfold Nat.ltb in *. simpl in *.
   discriminate. auto with arith.
   auto with arith.
 Defined.
diff --git a/theories/common/exceptionMonad.v b/theories/common/exceptionMonad.v
index 098a9db6..4ad1a22e 100644
--- a/theories/common/exceptionMonad.v
+++ b/theories/common/exceptionMonad.v
@@ -5,11 +5,11 @@ Import MonadNotation.
 
 Inductive exception (A:Type) := Exc (_:string) | Ret (_:A).
 Arguments Ret [A].
-Arguments Exc [A] _%bs.
+Arguments Exc [A] _%_bs.
 
 Definition ret {A: Type} (x: A) := Ret x.
 Definition raise {A: Type} (str:string) := @Exc A str.
-Arguments raise {A} _%bs.
+Arguments raise {A} _%_bs.
 
 Definition bind
     {A B: Type} (a: exception A) (f: A -> exception B): exception B :=