diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 31e2c324..14987d1e 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -18,7 +18,7 @@ jobs:
         opam_file:
           - 'coq-certicoq.opam'
         image:
-          - 'mattam82/metacoq:metacoq-1.3.2-coq-8.19'
+          - 'mattam82/metacoq:metacoq-1.3.4-coq-8.20'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v3
diff --git a/Makefile b/Makefile
index d887706b..76b7f72f 100644
--- a/Makefile
+++ b/Makefile
@@ -2,8 +2,8 @@
 
 
 all theories/Extraction/extraction.vo: theories/Makefile libraries/Makefile
-	$(MAKE) -C libraries -j1
-	$(MAKE) -C theories -j1
+	$(MAKE) -C libraries 
+	$(MAKE) -C theories 
 
 theories/Makefile: theories/_CoqProject
 	cd theories;coq_makefile -f _CoqProject -o Makefile
diff --git a/benchmarks/certicoq_eval_issue.v b/benchmarks/certicoq_eval_issue.v
index 4ffdca6a..8c45c23f 100644
--- a/benchmarks/certicoq_eval_issue.v
+++ b/benchmarks/certicoq_eval_issue.v
@@ -32,7 +32,7 @@ Import ListNotations.
 Definition l : list nat := map (fun x => x * x) (repeat 3 4000).
 
 Lemma nth_l : 3000 < length l.
-Proof. unfold l. rewrite map_length. rewrite repeat_length. Admitted.
+Proof. unfold l. rewrite length_map. rewrite repeat_length. Admitted.
 
 Definition test : nat := (nth l (3000; nth_l)).
 (* Time Eval vm_compute in test. *)
diff --git a/benchmarks/lib/Color.v b/benchmarks/lib/Color.v
index 866df07f..73692429 100755
--- a/benchmarks/lib/Color.v
+++ b/benchmarks/lib/Color.v
@@ -230,9 +230,9 @@ Proof.
 intros.
 do 2 rewrite M.cardinal_1.
 transitivity (length (map (@fst _ _) (M.elements (M.map f g)))).
-rewrite map_length; auto.
+rewrite length_map; auto.
 transitivity (length (map (@fst _ _) (M.elements g))).
-2: rewrite map_length; auto.
+2: rewrite length_map; auto.
 apply eqlistA_length with E.eq.
 apply SortE_equivlistE_eqlistE; auto.
 generalize (M.elements_3 (M.map f g)).
diff --git a/benchmarks/lib/vs.v b/benchmarks/lib/vs.v
index 44f1e1f9..77b2f912 100755
--- a/benchmarks/lib/vs.v
+++ b/benchmarks/lib/vs.v
@@ -425,9 +425,9 @@ pure atoms *)
 
 Inductive pure_atom := Eqv : expr -> expr -> pure_atom.
 
-Let var1 : var := Z2id 1.
-Let var0 : var := Z2id 0.
-Let var2 : var := Z2id 2.
+Definition var1 : var := Z2id 1.
+Definition var0 : var := Z2id 0.
+Definition var2 : var := Z2id 2.
 
 Fixpoint list_prio {A} (weight: var) (l: list A) (p: var) : var :=
   match l with
diff --git a/benchmarks/metacoq_erasure/certiCoqErase.ml b/benchmarks/metacoq_erasure/certiCoqErase.ml
index bcfc9cb6..9c48986a 100644
--- a/benchmarks/metacoq_erasure/certiCoqErase.ml
+++ b/benchmarks/metacoq_erasure/certiCoqErase.ml
@@ -58,7 +58,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   let open List in
   let rec aux p = 
   match p with
-  | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ | Coq_tInt _ | Coq_tFloat _ -> p
+  | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ | Coq_tInt _ | Coq_tFloat _ | tString _ -> p
   | Coq_tEvar (k, l) -> Coq_tEvar (k, map aux l)
   | Coq_tSort u -> Coq_tSort (fix_universe u)
   | Coq_tCast (t, k, t') -> Coq_tCast (aux t, k, aux t')
@@ -136,4 +136,4 @@ let erase ~bypass env evm c =
   debug (fun () -> str"Quoting");
   let prog = time (str"Quoting") (quote_term_rec ~bypass ~with_universes:false env) evm (EConstr.to_constr evm c) in
   let prog = fix_quoted_program prog in
-  time (str"Erasure") certicoq_erase prog
\ No newline at end of file
+  time (str"Erasure") certicoq_erase prog
diff --git a/bootstrap/certicoqc/Makefile b/bootstrap/certicoqc/Makefile
index b7373893..8766d189 100644
--- a/bootstrap/certicoqc/Makefile
+++ b/bootstrap/certicoqc/Makefile
@@ -56,7 +56,7 @@ COQLIB = $(shell coqc -where)
 COQLIBINSTALL = $(COQLIB)/user-contrib/CertiCoq/CertiCoqC
 OCAMLLIB = $(shell ocamlc -where)
 OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_plugin -package coq-certicoq-vanilla.plugin -open Certicoq_vanilla_plugin \
-	-I . -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8
+	-I . -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  
 GENCFILES = glue.c CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
 CFILES = certicoqc_wrapper.c $(GENCFILES)
 
@@ -86,7 +86,7 @@ test.vo: test.v
 	mkdir -p tests
 	ulimit -a
 	ulimit -H -a
-	ulimit -Ss 65500 && coqc $(TESTCOQOPTS) test.v
+	ulimit -Ss unlimited && ulimit -s unlimited && coqc $(TESTCOQOPTS) test.v
 
 clean: Makefile.certicoqc
 	make -f Makefile.certicoqc clean
diff --git a/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml b/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml
index 34039c2a..7fe89ab7 100644
--- a/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml
+++ b/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml
@@ -79,6 +79,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i)
   | Coq_tInt i -> Coq_tInt i
   | Coq_tFloat f -> Coq_tFloat f
+  | Coq_tString f -> Coq_tString f
   | Coq_tArray (u, v, def, ty) -> Coq_tArray (u, map aux v, aux def, aux ty)
   and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } =
     { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn }
@@ -171,4 +172,4 @@ let compile opts prog =
   let res = certicoq_pipeline opts prog in
   info "Certicoq pipeline ran";
   (* print_obj 10 (Obj.repr (fst res)); *)
-  res
\ No newline at end of file
+  res
diff --git a/bootstrap/certicoqc/test.v b/bootstrap/certicoqc/test.v
index 320c4d8d..7d005e96 100644
--- a/bootstrap/certicoqc/test.v
+++ b/bootstrap/certicoqc/test.v
@@ -47,4 +47,6 @@ CertiCoqC Eval demo2. *)
 
 (* Time CertiCoqC Compile -build_dir "tests" -time -O 1 demo1. *)
 
+Require Import Coq.Strings.PrimString.
+
 Time CertiCoqC Compile -build_dir "tests" -time -O 1 certicoqc.
diff --git a/bootstrap/certicoqchk/Makefile b/bootstrap/certicoqchk/Makefile
index 205acf59..c8f081a7 100644
--- a/bootstrap/certicoqchk/Makefile
+++ b/bootstrap/certicoqchk/Makefile
@@ -37,7 +37,7 @@ GENCFILES = glue.c CertiCoq.CertiCoqCheck.compile.certicoqchk.c
 CFILES = certicoqchk_wrapper.c ${GENCFILES}
 
 RUNTIME_DIR = ../../runtime
-RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_ffi.o
+RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_string.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_ffi.o
 
 CCOMPILEROPTS = -fPIC -g -c -I . -I ${RUNTIME_DIR} -I ${OCAMLLIB} -w -Wno-everything -O2
 # ccomp: CCOMPILEROPTS = -g -c -I . -I ${OCAMLLIB} -O2
@@ -103,4 +103,4 @@ install: Loader.vo certicoqchk_plugin.cmxs
 
 .PHONY: plugin test
 
-.NOTPARALLEL:
\ No newline at end of file
+.NOTPARALLEL:
diff --git a/coq-certicoq.opam b/coq-certicoq.opam
index 02e23548..a7dd2419 100644
--- a/coq-certicoq.opam
+++ b/coq-certicoq.opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev+8.19"
+version: "dev+8.20"
 maintainer: "The CertiCoq Team"
 homepage: "https://certicoq.org/"
 dev-repo: "git+https://github.com/CertiCoq/certicoq"
@@ -31,11 +31,11 @@ depends: [
   "ocaml" {>= "4.13"}
   "conf-clang"
   "stdlib-shims"
-  "coq" {>= "8.19" & < "8.20~"}
+  "coq" {>= "8.20" & < "8.21~"}
   "coq-compcert" {= "3.13.1"}
-  "coq-equations" {= "1.3+8.19"}
-  "coq-metacoq-erasure-plugin" {= "1.3.2+8.19"}
-  "coq-metacoq-safechecker-plugin" {= "1.3.2+8.19"}
+  "coq-equations" {= "1.3.1+8.20"}
+  "coq-metacoq-erasure-plugin" {= "1.3.4+8.20"}
+  "coq-metacoq-safechecker-plugin" {= "1.3.4+8.20"}
   "coq-ext-lib" {>= "0.12"}
 ]
 
diff --git a/cplugin/CertiCoqVanilla.v b/cplugin/CertiCoqVanilla.v
index ed54d2fa..22936e8a 100644
--- a/cplugin/CertiCoqVanilla.v
+++ b/cplugin/CertiCoqVanilla.v
@@ -1,2 +1,2 @@
 From CertiCoq.VanillaPlugin Require Import Loader.
-From CertiCoq.VanillaPlugin Require Export CoqMsgFFI PrimInt63 PrimFloats.
+From CertiCoq.VanillaPlugin Require Export CoqMsgFFI PrimInt63 PrimFloats PrimString.                            
diff --git a/cplugin/PrimString.v b/cplugin/PrimString.v
new file mode 100644
index 00000000..477ae1b3
--- /dev/null
+++ b/cplugin/PrimString.v
@@ -0,0 +1,10 @@
+From CertiCoq.VanillaPlugin Require Import Loader.
+From Coq Require Import PString.
+
+CertiCoq Register [
+  Coq.Strings.PrimString.compare => "prim_string_compare",
+  Coq.Strings.PrimString.get => "prim_string_get",
+  Coq.Strings.PrimString.length => "prim_string_length"
+]
+Include [ Library "prim_string.h" ].
+
diff --git a/cplugin/_CoqProject b/cplugin/_CoqProject
index 5ccdc7ba..cd0366c1 100644
--- a/cplugin/_CoqProject
+++ b/cplugin/_CoqProject
@@ -19,6 +19,7 @@ Loader.v
 CoqMsgFFI.v
 PrimInt63.v
 PrimFloats.v
+PrimString.v
 CertiCoqVanilla.v
 
 static/caml_option.mli
@@ -389,6 +390,10 @@ extraction/primFloat.ml
 extraction/primFloat.mli
 extraction/primInt63.ml
 extraction/primInt63.mli
+extraction/primString.ml
+extraction/primString.mli
+extraction/primStringAxioms.ml
+extraction/primStringAxioms.mli
 extraction/primitive.ml
 extraction/primitive.mli
 extraction/proto_util.ml
diff --git a/cplugin/certicoq.ml b/cplugin/certicoq.ml
index 312fab69..2185a899 100644
--- a/cplugin/certicoq.ml
+++ b/cplugin/certicoq.ml
@@ -427,6 +427,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i)
   | Coq_tInt i -> p
   | Coq_tFloat f -> p
+  | Coq_tString s -> p
   | Coq_tArray (u, v, def, ty) -> Coq_tArray (u, map aux v, aux def, aux ty)
   and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } =
     { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn }
@@ -782,7 +783,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
   let check_reifyable env sigma ty =
     (* We might have bound universes though. It's fine! *)
     try let (hd, u), args = Inductiveops.find_inductive env sigma ty in
-      IsInductive (hd, EConstr.EInstance.kind sigma u, args)
+      IsInductive (hd, EConstr.EInstance.kind sigma u, List.map (EConstr.to_constr sigma) args)
     with Not_found -> 
       let hnf = Reductionops.whd_all env sigma ty in
       let hd, args = EConstr.decompose_app sigma hnf in
@@ -856,7 +857,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let spec = lookup_mind_specif env hd in
       let npars = inductive_params spec in
       let params, _indices = CList.chop npars args in
-      let indfam = make_ind_family ((hd, u), params) in
+      let indfam = make_ind_family ((hd, EConstr.EInstance.make u), List.map (EConstr.of_constr) params) in
       let cstrs = get_constructors env indfam in
       let cstrs = apply_reordering qhd im cstrs in
       if Obj.is_block v then
@@ -868,7 +869,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
         in
         let cstr = cstrs.(coqidx) in
         let coqidx = find_reverse_mapping qhd im coqidx in
-        let ctx = Vars.smash_rel_context cstr.cs_args in
+        let ctx = Vars.smash_rel_context (EConstr.to_rel_context sigma cstr.cs_args) in
         let vargs = List.init (List.length ctx) (Obj.field v) in
         let args' = List.map2 (fun decl v -> 
           let argty = check_reifyable env sigma 
diff --git a/cplugin/certicoq_vanilla_plugin.mlpack b/cplugin/certicoq_vanilla_plugin.mlpack
index 738163aa..82ffb7e1 100644
--- a/cplugin/certicoq_vanilla_plugin.mlpack
+++ b/cplugin/certicoq_vanilla_plugin.mlpack
@@ -23,6 +23,8 @@ BinNat
 BinInt
 PrimInt63
 Uint0
+PrimString
+PrimStringAxioms
 Int0
 Int63
 Byte
diff --git a/plugin/CertiCoq.v b/plugin/CertiCoq.v
index ca9fefeb..f929e9b8 100644
--- a/plugin/CertiCoq.v
+++ b/plugin/CertiCoq.v
@@ -1,2 +1,2 @@
 From CertiCoq.Plugin Require Export Loader.
-From CertiCoq.Plugin Require Export CoqMsgFFI PrimInt63 PrimFloats.
\ No newline at end of file
+From CertiCoq.Plugin Require Export CoqMsgFFI PrimInt63 PrimFloats PrimString.
diff --git a/plugin/PrimString.v b/plugin/PrimString.v
new file mode 100644
index 00000000..88bbcd9a
--- /dev/null
+++ b/plugin/PrimString.v
@@ -0,0 +1,10 @@
+From CertiCoq.Plugin Require Import Loader.
+From Coq Require Import PString.
+
+CertiCoq Register [
+    Coq.Strings.PrimString.compare => "prim_string_compare",
+      Coq.Strings.PrimString.get => "prim_string_get",
+      Coq.Strings.PrimString.length => "prim_string_length"
+  ]
+  Include [ Library "prim_string.h" ].
+
diff --git a/plugin/_CoqProject b/plugin/_CoqProject
index 6c77301f..cb1153cd 100644
--- a/plugin/_CoqProject
+++ b/plugin/_CoqProject
@@ -19,6 +19,7 @@ Loader.v
 CoqMsgFFI.v
 PrimInt63.v
 PrimFloats.v
+PrimString.v
 CertiCoq.v
 
 static/caml_nat.mli
@@ -386,6 +387,10 @@ extraction/primInt63.ml
 extraction/primInt63.mli
 extraction/primitive.ml
 extraction/primitive.mli
+extraction/primString.ml
+extraction/primString.mli
+extraction/primStringAxioms.ml
+extraction/primStringAxioms.mli
 extraction/proto_util.ml
 extraction/proto_util.mli
 extraction/prototype.ml
diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml
index 99879168..f8384475 100644
--- a/plugin/certicoq.ml
+++ b/plugin/certicoq.ml
@@ -644,7 +644,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
   let check_reifyable env sigma ty =
     (* We might have bound universes though. It's fine! *)
     try let (hd, u), args = Inductiveops.find_inductive env sigma ty in
-      IsInductive (hd, EConstr.EInstance.kind sigma u, args)
+      IsInductive (hd, EConstr.EInstance.kind sigma u, List.map (EConstr.to_constr sigma) args)
     with Not_found -> 
       let hnf = Reductionops.whd_all env sigma ty in
       let hd, args = EConstr.decompose_app sigma hnf in
@@ -718,7 +718,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let spec = lookup_mind_specif env hd in
       let npars = inductive_params spec in
       let params, _indices = CList.chop npars args in
-      let indfam = make_ind_family ((hd, u), params) in
+      let indfam = make_ind_family ((hd, EConstr.EInstance.make u), List.map (EConstr.of_constr) params) in
       let cstrs = get_constructors env indfam in
       let cstrs = apply_reordering qhd im cstrs in
       if Obj.is_block v then
@@ -730,7 +730,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
         in
         let cstr = cstrs.(coqidx) in
         let coqidx = find_reverse_mapping qhd im coqidx in
-        let ctx = Vars.smash_rel_context cstr.cs_args in
+        let ctx = Vars.smash_rel_context (EConstr.to_rel_context sigma cstr.cs_args) in
         let vargs = List.init (List.length ctx) (Obj.field v) in
         let args' = List.map2 (fun decl v -> 
           let argty = check_reifyable env sigma 
diff --git a/plugin/certicoq_plugin.mlpack b/plugin/certicoq_plugin.mlpack
index 4965722f..2960195a 100644
--- a/plugin/certicoq_plugin.mlpack
+++ b/plugin/certicoq_plugin.mlpack
@@ -23,6 +23,8 @@ PrimInt63
 Uint0
 Int0
 Int63
+PrimString
+PrimStringAxioms
 Byte
 Caml_byte
 Ascii
diff --git a/runtime/prim_int63.c b/runtime/prim_int63.c
index 9dd891ba..32dd6d05 100644
--- a/runtime/prim_int63.c
+++ b/runtime/prim_int63.c
@@ -7,7 +7,7 @@ typedef value primbool;
 typedef value primintcarry;
 typedef value primintpair;
 
-#define trace(...) // printf(__VA_ARGS__)
+#define trace(...) printf(__VA_ARGS__)
 
 #define maxuint63 0x7FFFFFFFFFFFFFFF
 
diff --git a/runtime/prim_string.c b/runtime/prim_string.c
new file mode 100644
index 00000000..aa9a929f
--- /dev/null
+++ b/runtime/prim_string.c
@@ -0,0 +1,47 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "gc_stack.h"
+#include "prim_int63.h"
+
+typedef value primstring;
+
+#define trace(...) printf(__VA_ARGS__)
+
+value prim_string_compare(primstring x, primstring y)
+{
+  /* register signed long long xr = Unsigned_long_val(x); */
+  /* register signed long long yr = Unsigned_long_val(y); */
+  /* register signed long long result = xr - yr; */
+  trace("Calling prim_string_compare\n");
+  /* trace("Calling prim_string_compare on %llu and %llu: %lli \n", x, y); */
+  /* if (result == 0) return 1; */
+  /* else if (result < 0) return 3; */
+  /* else */
+    return 1;
+}
+
+primint prim_string_get(primstring x, primint y)
+{
+  /* register signed long long xr = Unsigned_long_val(x); */
+  /* register signed long long yr = Unsigned_long_val(y); */
+  /* register signed long long result = xr - yr; */
+  trace("Calling prim_string_get\n");
+  /* trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); */
+  /* if (result == 0) return 1; */
+  /* else if (result < 0) return 3; */
+  /* else */
+    return 97;
+}
+
+primint prim_string_length(primstring x)
+{
+  /* register signed long long xr = Unsigned_long_val(x); */
+  /* register signed long long yr = Unsigned_long_val(y); */
+  /* register signed long long result = xr - yr; */
+  trace("Calling prim_string_length\n");
+  /* trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); */
+  /* if (result == 0) return 1; */
+  /* else if (result < 0) return 3; */
+  /* else */
+  return 0;
+}
diff --git a/runtime/prim_string.h b/runtime/prim_string.h
new file mode 100644
index 00000000..03b1e770
--- /dev/null
+++ b/runtime/prim_string.h
@@ -0,0 +1,8 @@
+#include "values.h"
+#include "prim_int63.h"
+
+typedef value primstring;
+
+extern value prim_string_compare(primstring x);
+extern primint prim_string_get(primstring x, primint y);
+extern value prim_string_length(primstring x);
diff --git a/submodules/metacoq b/submodules/metacoq
index b1b6be23..9af0b0fc 160000
--- a/submodules/metacoq
+++ b/submodules/metacoq
@@ -1 +1 @@
-Subproject commit b1b6be23e00fefba6a03c153a458e72acb463daa
+Subproject commit 9af0b0fc7b8c3a2989aae8a11e6a6b24695128ef
diff --git a/theories/Codegen/LambdaANF_to_Clight_correct.v b/theories/Codegen/LambdaANF_to_Clight_correct.v
index 6e04e565..e73687bb 100644
--- a/theories/Codegen/LambdaANF_to_Clight_correct.v
+++ b/theories/Codegen/LambdaANF_to_Clight_correct.v
@@ -7842,8 +7842,8 @@ Proof.
                        destruct H2.
                        * revert H2. apply H_not_in_L.
                          int_red.
-                         rewrite app_length.
-                         rewrite rev_length.
+                         rewrite length_app.
+                         rewrite length_rev.
                          simpl length.
                          rewrite Nat2Z.inj_add.
                          rewrite Nat2Z.inj_succ. chunk_red; omega.                         
diff --git a/theories/Extraction/extraction.v b/theories/Extraction/extraction.v
index 377fbd41..f11cba24 100644
--- a/theories/Extraction/extraction.v
+++ b/theories/Extraction/extraction.v
@@ -16,7 +16,7 @@ Require Glue.glue
 
 From MetaCoq.ErasurePlugin Require Import Erasure.
 (* Standard lib *)
-Require Import ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63.
+Require Import ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63 ExtrOCamlPString.
 Require Import Coq.extraction.Extraction.
 Require Import ZArith NArith.
 
diff --git a/theories/ExtractionVanilla/extraction.v b/theories/ExtractionVanilla/extraction.v
index ecb6f531..ade13a10 100644
--- a/theories/ExtractionVanilla/extraction.v
+++ b/theories/ExtractionVanilla/extraction.v
@@ -15,7 +15,7 @@ Require Glue.glue
         Compiler.pipeline.
 
 Require Import Coq.extraction.Extraction.
-Require Import VanillaExtrOCamlInt63 VanillaExtrOCamlFloats.
+Require Import VanillaExtrOCamlInt63 VanillaExtrOCamlFloats ExtrOCamlPString.
 (* Standard lib *)
 
 (** Extraction to Ocaml : use of basic Ocaml types: be careful that this should 
diff --git a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v
index 3d2d5fbb..7f6da765 100644
--- a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v
+++ b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_correct.v
@@ -806,11 +806,11 @@ Section Correct.
       { erewrite cps_fix_rel_names; [ | eassumption ].
         rewrite H0. erewrite <- cps_fix_rel_length. reflexivity. eassumption. }
 
-      - eapply nth_error_Forall2; [ | rewrite rev_length; eassumption ].
+      - eapply nth_error_Forall2; [ | rewrite length_rev; eassumption ].
         intros.
         assert (exists f, nth_error (rev (all_fun_name Bs)) n = Some f).
         { eapply MCList.nth_error_Some_length in H2.
-          rewrite Hlen, <- rev_length in H2. eapply nth_error_Some in H2.
+          rewrite Hlen, <- length_rev in H2. eapply nth_error_Some in H2.
           destruct (nth_error (rev (all_fun_name Bs)) n); eauto. congruence. }
         destructAll.
         eexists. split. eauto.
@@ -1005,12 +1005,12 @@ Section Correct.
         intros vs. eapply MCList.rev_ind with (l := vs); intros.
 
         + eapply set_lists_length_eq in Hset.
-          rewrite app_length in Hset. inv Hset. lia.
+          rewrite length_app in Hset. inv Hset. lia.
           
         + simpl in Hset.
 
           assert (Hlen : Datatypes.length (rev vars) = Datatypes.length l). 
-          { eapply set_lists_length_eq in Hset. rewrite !app_length in Hset. simpl in *.
+          { eapply set_lists_length_eq in Hset. rewrite !length_app in Hset. simpl in *.
             replace (@Datatypes.length map_util.M.elt) with (@Datatypes.length positive) in * by reflexivity.
             lia. } 
 
@@ -1024,7 +1024,7 @@ Section Correct.
               2:{ intros m. eapply preord_exp_Eproj_red. eassumption.
                   eapply nthN_is_Some_app. 
                   eapply set_lists_length_eq in Hset.
-                  rewrite rev_length in *.
+                  rewrite length_rev in *.
                   replace (@Datatypes.length map_util.M.elt) with (@Datatypes.length positive) in * by reflexivity.
                   rewrite Hlen. rewrite nthN_app_geq. simpl.
                   
@@ -1981,7 +1981,7 @@ Section Correct.
                   - inv Hwfcl.
                     eapply enthopt_inlist_Forall in H26; [ | eassumption ].
                     inv H26. inv H22. simpl Datatypes.length.
-                    rewrite app_length, rev_length. erewrite cps_fix_rel_length; [ | eassumption ].
+                    rewrite length_app, length_rev. erewrite cps_fix_rel_length; [ | eassumption ].
                     erewrite <- Forall2_length; [ | eassumption ].
                     rewrite Nnat.Nat2N.inj_succ, <- OrdersEx.N_as_OT.add_1_l, Nnat.Nat2N.inj_add, efnlength_efnlst_length.
                     eassumption.
@@ -2031,7 +2031,7 @@ Section Correct.
           - inv Hwfcl.
             eapply enthopt_inlist_Forall in H26; [ | eassumption ].
             inv H26. inv H22. simpl Datatypes.length.
-            rewrite app_length, rev_length. erewrite cps_fix_rel_length; [ | eassumption ].
+            rewrite length_app, length_rev. erewrite cps_fix_rel_length; [ | eassumption ].
             erewrite <- Forall2_length; [ | eassumption ].
             rewrite Nnat.Nat2N.inj_succ, <- OrdersEx.N_as_OT.add_1_l, Nnat.Nat2N.inj_add, efnlength_efnlst_length.
             eassumption.
@@ -2084,7 +2084,7 @@ Section Correct.
                                     (M.set k1 (Vfun rho (Fcons k1 kon_tag [x1] (Ecase x1 bs') Fnil) k1) rho)).
               
         edestruct (set_lists_length3 rho' (rev x2) vs'0).
-        { rewrite rev_length. rewrite H5, Nnat.Nat2N.id. eapply Forall2_length. eassumption. } 
+        { rewrite length_rev. rewrite H5, Nnat.Nat2N.id. eapply Forall2_length. eassumption. } 
         destructAll. 
 
 
@@ -2163,7 +2163,7 @@ Section Correct.
               2:{ intros i. eapply IH2 ; [ | | | | | | | eassumption | reflexivity | eassumption ]. 
                   - eapply Forall_app. split; eauto.
                     eapply Forall_rev. inv Hvwf. eassumption.
-                  - rewrite app_length, Nnat.Nat2N.inj_add. 
+                  - rewrite length_app, Nnat.Nat2N.inj_add. 
                     eapply cps_cvt_rel_branches_find_branch_wf. eassumption.
                     eassumption. rewrite H5. eassumption.
                   - normalize_sets.
@@ -2233,7 +2233,7 @@ Section Correct.
           edestruct IH2 ; [ | | | | | | | eassumption | ]. 
           - eapply Forall_app. split; eauto.
             eapply Forall_rev. inv Hvwf. eassumption.
-          - rewrite app_length, Nnat.Nat2N.inj_add. 
+          - rewrite length_app, Nnat.Nat2N.inj_add. 
             eapply cps_cvt_rel_branches_find_branch_wf. eassumption.
             eassumption. rewrite H5. eassumption.
           - normalize_sets.
@@ -2627,12 +2627,12 @@ Section Correct.
               * constructor.
                 -- intros Hc. eapply in_app_or in Hc. inv Hc; eauto.
                    eapply in_rev in H17; eauto.
-                -- eapply NoDup_app; eauto.
+                -- eapply List_util.NoDup_app; eauto.
                    eapply NoDup_rev. eassumption.
                    rewrite FromList_rev. sets.
               * repeat normalize_sets. rewrite FromList_rev.
                 intros Hc. inv Hc. inv H17; eauto. inv H17; eauto.
-              * simpl. rewrite !app_length, !rev_length.
+              * simpl. rewrite !length_app, !length_rev.
                 rewrite H3. erewrite <- cps_fix_rel_length; [ | eassumption ]. congruence. 
               * repeat normalize_sets. rewrite FromList_rev.
                 eapply Union_Disjoint_l. now sets.
@@ -2689,7 +2689,7 @@ Section Correct.
                 -- replace (@Datatypes.length positive) with (@Datatypes.length var) in * by reflexivity.
                    rewrite H3. eapply cps_fix_rel_length; eauto.
                    
-                -- rewrite !rev_length.
+                -- rewrite !length_rev.
                    rewrite H3. eapply cps_fix_rel_length; eauto.
 
                 -- intros Hc. eapply image_extend_lst_Included in Hc; eauto. rewrite image_id in Hc.
@@ -2700,7 +2700,7 @@ Section Correct.
                    rewrite Hseq in Hc. repeat normalize_sets. inv Hc; eauto. 
                    now eapply Same_set_all_fun_name in H17; inv H4; eauto.
                    now inv H4; eapply Hdis; eauto.
-                   rewrite !app_length, !rev_length.
+                   rewrite !length_app, !length_rev.
                    erewrite H3, <- cps_fix_rel_length; [ | eassumption ]. congruence. 
 
                 -- intros Hc. eapply image_extend_Included' in Hc. inv Hc; eauto. 
@@ -2712,7 +2712,7 @@ Section Correct.
                    rewrite Hseq in H17. repeat normalize_sets. inv H17; eauto. 
                    now eapply Same_set_all_fun_name in H24; inv H12; inv H17; eauto.
                    now inv H12; inv H17; eapply Hdis; eauto.
-                   rewrite !app_length, !rev_length.
+                   rewrite !length_app, !length_rev.
                    erewrite H3, <- cps_fix_rel_length; [ | eassumption ]. congruence.
                    inv H17; inv H12; eauto.
                    
@@ -2728,7 +2728,7 @@ Section Correct.
                    intros Hc. eapply in_app_or in Hc. inv Hc.
                    eapply in_rev in H17; eauto. eapply Hdis; eauto.
 
-                -- rewrite !app_length, !rev_length.
+                -- rewrite !length_app, !length_rev.
                    erewrite H3, <- cps_fix_rel_length; [ | eassumption ]. congruence. } 
 
         
diff --git a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_corresp.v b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_corresp.v
index 735d2b42..57f1e43e 100644
--- a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_corresp.v
+++ b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_corresp.v
@@ -347,8 +347,8 @@ Section Corresp.
       eapply pre_strenghtening.
       2:{ eapply post_weakening.
           2:{ eapply H. eassumption.
-              rewrite Hlen. rewrite map_length. eassumption.
-              rewrite Hlen'. rewrite map_length. eassumption. }
+              rewrite Hlen. rewrite length_map. eassumption.
+              rewrite Hlen'. rewrite length_map. eassumption. }
           simpl. intros. destructAll.
           eexists. split. econstructor; try eassumption. reflexivity.
           eassumption. }
@@ -457,11 +457,11 @@ Section Corresp.
       
       eapply frame_rule. eapply frame_rule. 
 
-      eapply H. rewrite app_length, rev_length. unfold fnames in Hlen.
-      rewrite map_length in Hlen. rewrite Hlen. 
+      eapply H. rewrite length_app, length_rev. unfold fnames in Hlen.
+      rewrite length_map in Hlen. rewrite Hlen. 
       
       rewrite Nnat.Nat2N.inj_add. rewrite Hlen'. eassumption.
-      rewrite Hlen. unfold fnames. rewrite map_length.
+      rewrite Hlen. unfold fnames. rewrite length_map.
       rewrite <- Nnat.Nat2N.id with (n := Datatypes.length (efnlst_as_list e)).
       rewrite <- Nnat.Nat2N.id with (n := efnlength e).
       rewrite Hlen', efnlength_efnlst_length. reflexivity.
@@ -471,7 +471,7 @@ Section Corresp.
       destruct (nth_error x (N.to_nat n)) eqn:Hnth.
       + eapply return_triple. intros _ w3 Hf. destructAll. 
         eexists. split.
-        * econstructor; eauto. rewrite Hlen. unfold fnames. rewrite map_length.
+        * econstructor; eauto. rewrite Hlen. unfold fnames. rewrite length_map.
           rewrite <- Nnat.Nat2N.id with (n := Datatypes.length (efnlst_as_list e)).
           rewrite <- Nnat.Nat2N.id with (n := efnlength e).
           rewrite Hlen'. rewrite efnlength_efnlst_length. reflexivity.
@@ -479,7 +479,7 @@ Section Corresp.
         * eassumption.
 
       + eapply nth_error_Some in Hnth. now exfalso; eauto.
-        rewrite Hlen. unfold fnames. rewrite map_length. 
+        rewrite Hlen. unfold fnames. rewrite length_map. 
         rewrite <- Nnat.Nat2N.id with (n := Datatypes.length (efnlst_as_list e)).          
         rewrite Hlen'. lia.
 
@@ -622,7 +622,7 @@ Section Corresp.
       eapply frame_rule. eapply frame_rule. 
 
       eapply H. simpl in *.
-      rewrite app_length. rewrite Hnd, names_lst_length.
+      rewrite length_app. rewrite Hnd, names_lst_length.
       rewrite Nnat.Nat2N.inj_add. rewrite Nnat.N2Nat.id. eassumption.
 
       intros e2 w3. eapply return_triple. intros. destructAll.  
@@ -764,7 +764,7 @@ Section Corresp.
 
       inv H4.
       assert (Hwf : exp_wf (N.of_nat (Datatypes.length (y :: (rev fnames ++ names)))) e).
-      { simpl. rewrite app_length in *. rewrite rev_length.
+      { simpl. rewrite length_app in *. rewrite length_rev.
         replace (N.pos (Pos.of_succ_nat (Datatypes.length fnames + Datatypes.length names)))
           with (1 + N.of_nat (Datatypes.length fnames + Datatypes.length names)) by lia.
         eassumption. }
@@ -915,7 +915,7 @@ Section Corresp.
       { unfold fnames. rewrite pos_seq_len. lia. }
       
       assert (Hwf : efnlst_wf (N.of_nat (Datatypes.length (fnames ++ names))) fnl).
-      { revert H5. rewrite app_length, Nnat.Nat2N.inj_add, Hlen.
+      { revert H5. rewrite length_app, Nnat.Nat2N.inj_add, Hlen.
         unfold names. rewrite pos_seq_len. generalize (N.of_nat (Datatypes.length fnames) + N.of_nat (Datatypes.length vs)).
         clear. induction fnl; intros m Hall.
         - constructor.
diff --git a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v
index 098f5653..7d0f3e8e 100644
--- a/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v
+++ b/theories/LambdaANF/LambdaBoxLocal_to_LambdaANF_util.v
@@ -340,7 +340,7 @@ Section Post.
 
           * congruence.
 
-          * rewrite !app_length. simpl. congruence. 
+          * rewrite !length_app. simpl. congruence. 
 
           * congruence.
           * eassumption.
@@ -701,8 +701,8 @@ Section Post.
         rewrite IHxs; eauto. reflexivity. 
         intros Hc. now eapply in_rev in Hc; eauto. 
         intros Hc. now eapply in_rev in Hc; eauto.
-        rewrite !rev_length. congruence.
-        rewrite !rev_length. congruence.
+        rewrite !length_rev. congruence.
+        rewrite !length_rev. congruence.
     Qed.        
     
     Ltac inv_setminus :=
@@ -1389,7 +1389,7 @@ Section Post.
                   rewrite <- extend_lst_rev.
                   eapply IH; try eassumption. reflexivity. reflexivity.
                   
-                  - eapply NoDup_app; eauto.
+                  - eapply List_util.NoDup_app; eauto.
                     now eapply NoDup_rev; eauto. 
                     
                     eapply Disjoint_sym. rewrite FromList_rev.
@@ -1518,7 +1518,7 @@ Section Post.
                     - eassumption. 
                     - inv Hdup2. eassumption.
                     - inv Hdup3. eassumption.
-                    - apply NoDup_app. eassumption.
+                    - apply List_util.NoDup_app. eassumption.
                       constructor. intros Hc. now inv Hc. now constructor.
                       repeat normalize_sets. sets.
                     - inv Hnd5. eassumption.                      
@@ -1528,7 +1528,7 @@ Section Post.
                     - repeat normalize_sets. xsets.
                     - congruence.
                     - congruence.
-                    - rewrite !app_length. simpl. congruence.
+                    - rewrite !length_app. simpl. congruence.
                     - repeat normalize_sets. eapply Disjoint_Included_r.
                       eapply cps_cvt_exp_subset. eassumption. repeat normalize_sets. xsets.
                       
@@ -1713,7 +1713,7 @@ Section Post.
               + repeat normalize_sets. inv H6. intros Hc. inv Hc.
                 * inv H6. eauto.
                 * eapply Hdis1. now sets.
-              + simpl. rewrite !app_length, !rev_length. congruence.
+              + simpl. rewrite !length_app, !length_rev. congruence.
               + repeat normalize_sets.
                 eapply Union_Disjoint_l; sets.
                 eapply Union_Disjoint_l; sets.
@@ -1735,7 +1735,7 @@ Section Post.
                   - inv H12. intros Hc. eapply Hdis2. rewrite FromList_rev. 
                     eapply in_app_or in Hc. inv Hc; eauto.
                     eapply in_rev in H12; eauto.
-                  - rewrite !app_length. rewrite !rev_length. congruence. }
+                  - rewrite !length_app. rewrite !length_rev. congruence. }
                 
                 rewrite Hfeq. 
                 
@@ -1757,20 +1757,20 @@ Section Post.
 
                   rewrite extend_lst_app.
                   
-                  eapply f_eq_subdomain_extend_lst. rewrite !rev_length.  eassumption.
+                  eapply f_eq_subdomain_extend_lst. rewrite !length_rev.  eassumption.
                   eapply f_eq_subdomain_extend_lst. eassumption.
                   
                   
                   assert (Hfeq' : (x |: (x0 |: (FromList (rev (all_fun_name B1)) :|: FromList vars1')) \\ [set x] \\ [set x0] \\
                                      FromList (rev (all_fun_name B1)) \\ FromList vars1') <--> Empty_set _) by xsets.
-                  rewrite Hfeq'. intros z Hinz. now inv Hinz. rewrite !rev_length. eassumption. 
+                  rewrite Hfeq'. intros z Hinz. now inv Hinz. rewrite !length_rev. eassumption. 
                   
                 * intros Hc. eapply image_extend_lst_Included in Hc; eauto.
                   rewrite image_id in Hc. inv Hc; eauto. inv H9; eauto. inv H15; eauto. 
                   inv H9; eauto. inv H15; eauto. repeat normalize_sets. now inv H9; eauto.
 
                   repeat normalize_sets. eapply Hdis2. now sets.
-                  rewrite !app_length, !rev_length. congruence.
+                  rewrite !length_app, !length_rev. congruence.
                   
                 * intros Hc. eapply image_extend_Included' in Hc.
                   inv H12. inv Hc; eauto.
@@ -1784,7 +1784,7 @@ Section Post.
                   
                   rewrite Heq in H12. repeat normalize_sets.
                   now eapply Hdis2; eauto.
-                  rewrite !app_length, !rev_length. congruence. } 
+                  rewrite !length_app, !length_rev. congruence. } 
           
       - (* brnil_e *)
         intros bs1 bs2 m k1 k2 vars1 vars2 x1 x2 rho1 rho2
@@ -1832,12 +1832,12 @@ Section Post.
 
             -- intros. eapply IHe; try eassumption. lia.
                
-               ++ eapply NoDup_app; eauto.
+               ++ eapply List_util.NoDup_app; eauto.
                   eapply Disjoint_Included_l. eassumption. sets.
                   
                ++ repeat normalize_sets.
                   intros Hc. inv Hc; eauto. eapply Hdis1. now eauto.
-               ++ rewrite !app_length. congruence.
+               ++ rewrite !length_app. congruence.
                ++ eapply cps_cvt_rel_subset in H16.
                   repeat normalize_sets.
                   eapply Union_Disjoint_l; sets.
@@ -2161,11 +2161,11 @@ Section Post.
         + eassumption.
         + constructor; eauto.
           intros Hc. eapply in_app_or in Hc. inv Hc; eauto. now eapply in_rev in H0; eauto.
-          eapply NoDup_app; eauto. eapply NoDup_rev. eassumption.
+          eapply List_util.NoDup_app; eauto. eapply NoDup_rev. eassumption.
           rewrite FromList_rev. sets.
         + repeat normalize_sets. intros Hc; inv Hc; eauto.
           inv H0; eauto. rewrite FromList_rev in H0. eauto.
-        + simpl. rewrite !app_length, !rev_length. congruence.
+        + simpl. rewrite !length_app, !length_rev. congruence.
         + repeat normalize_sets.
           eapply Union_Disjoint_l; sets. 
           eapply Union_Disjoint_l; sets.
@@ -2206,7 +2206,7 @@ Section Post.
             eapply Forall_impl; [ | eassumption ]. simpl. intros.
             eapply preord_val_monotonic. eapply H26. eassumption. eassumption. lia.            
 
-          * rewrite !rev_length. eassumption. 
+          * rewrite !length_rev. eassumption. 
             
           * intros Hc. eapply image_extend_lst_Included in Hc. repeat normalize_sets. rewrite image_id in Hc.
             rewrite !FromList_rev in Hc. 
@@ -2214,7 +2214,7 @@ Section Post.
                               (FromList (all_fun_name Bs) :|: FromList names) <--> Empty_set _) by xsets.
             rewrite Hseq in Hc. repeat normalize_sets.
             now inv Hc; eauto.
-            rewrite !app_length, !rev_length. congruence. 
+            rewrite !length_app, !length_rev. congruence. 
 
           * intros Hc. eapply image_extend_Included' in Hc.
             inv Hc; eauto. eapply image_extend_lst_Included in H0. repeat normalize_sets. rewrite image_id in H0.
@@ -2223,7 +2223,7 @@ Section Post.
                               (FromList (all_fun_name Bs) :|: FromList names) <--> Empty_set _) by xsets.
             rewrite Hseq in H0. repeat normalize_sets.
             now inv H0; eauto. 
-            rewrite !app_length, !rev_length. congruence.
+            rewrite !length_app, !length_rev. congruence.
             inv H0; eauto.
             
           * intros Hc; subst; eauto.
@@ -2234,7 +2234,7 @@ Section Post.
 
           * intros Hc. eapply in_app_or in Hc. inv Hc; eauto. eapply in_rev in H0; eauto.
 
-          * rewrite !app_length, !rev_length. congruence.
+          * rewrite !length_app, !length_rev. congruence.
     Qed.
 
 
diff --git a/theories/LambdaANF/Prototype.v b/theories/LambdaANF/Prototype.v
index 65045795..e011696c 100644
--- a/theories/LambdaANF/Prototype.v
+++ b/theories/LambdaANF/Prototype.v
@@ -149,6 +149,7 @@ Definition named_of' (Γ : list string) (tm : term) : GM term :=
       | tCoFix mfix idx => tCoFix <$> go_mfix mfix <*> ret idx
       | tInt i => ret (tInt i)
       | tFloat f => ret (tFloat f)
+      | tString s => ret (tString s)
       | tArray u v def ty => tArray u <$> mapM (go Γ) v <*> go Γ def <*> go Γ ty
       end
     end
@@ -245,6 +246,7 @@ Definition indices_of (Γ : list string) (t : term) : GM term :=
       | tInt i => ret (tInt i)
       | tFloat f => ret (tFloat f)
       | tArray _ _ _ _ => ret tm
+      | tString _ => ret tm
       end
     end
   in go 1000%nat [] t.
@@ -329,7 +331,7 @@ Definition rename (σ : Map string string) : term -> term :=
     | tProj proj t => tProj proj (go t)
     | tFix mfix idx => tFix (go_mfix mfix) idx
     | tCoFix mfix idx => tCoFix (go_mfix mfix) idx
-    | tInt _ | tFloat _ => tm
+    | tInt _ | tFloat _ | tString _ => tm
     | tArray u v def ty => tArray u (map go v) (go def) (go ty)
     end.
 
@@ -713,7 +715,7 @@ Fixpoint vars_of (t : term) : Set' string :=
   | tProj proj t => vars_of t
   | tFix mfix idx => union_all (map (fun def => vars_of def.(dtype) ∪ vars_of def.(dbody)) mfix)
   | tCoFix mfix idx => union_all (map (fun def => vars_of def.(dtype) ∪ vars_of def.(dbody)) mfix)
-  | tInt _ | tFloat _ => empty
+  | tInt _ | tFloat _ | tString _ => empty
   | tArray u v def ty => vars_of def ∪ vars_of ty ∪ union_all (map vars_of v)
   end.
 
@@ -835,7 +837,7 @@ Fixpoint has_var (x : Kernames.ident) (e : term) {struct e} : bool. ltac1:(refin
   | tProj proj t => has_var x t
   | tFix mfix idx => anyb (fun d => has_var x d.(dtype) || has_var x d.(dbody)) mfix
   | tCoFix mfix idx => anyb (fun d => has_var x d.(dtype) || has_var x d.(dbody)) mfix
-  | tInt _ | tFloat _ => false
+  | tInt _ | tFloat _ | tString _ => false
   | tArray u v def ty => anyb (has_var x) v || has_var x def || has_var x ty
   end%bool
 )).
diff --git a/theories/LambdaANF/Rewriting.v b/theories/LambdaANF/Rewriting.v
index 7e641092..1b3f2dea 100644
--- a/theories/LambdaANF/Rewriting.v
+++ b/theories/LambdaANF/Rewriting.v
@@ -192,7 +192,7 @@ Notation "<[ x ; .. ; z ]>" := (frames_cons z .. (frames_cons x frames_nil) ..).
 Definition frames_t {U : Set} `{Frame U} : U -> U -> Set := frames_t' frame_t.
 
 (* Context application *)
-Reserved Notation "C '⟦' x '⟧'" (at level 50, no associativity).
+Reserved Notation "C '⟦' x '⟧'" (at level 1, no associativity).
 Fixpoint framesD {U : Set} `{Frame U} {A B : U}
          (fs : frames_t A B) : univD A -> univD B :=
   match fs with
diff --git a/theories/LambdaANF/closure_conversion_correct.v b/theories/LambdaANF/closure_conversion_correct.v
index d95c7784..c54f224a 100644
--- a/theories/LambdaANF/closure_conversion_correct.v
+++ b/theories/LambdaANF/closure_conversion_correct.v
@@ -888,7 +888,7 @@ Section Closure_conversion_correct.
           eapply project_vars_free_set_Included. eassumption.  
           
           apply Fun_inv_set_In_Scope_l. now eauto.
-          eapply Fun_inv_monotonic. eapply Fun_inv_mon. eassumption. lia.
+          eapply Fun_inv_monotonic. shelve. eapply Fun_inv_mon. eassumption. lia.
         * eapply FV_inv_set_In_Scope_l. now constructor.
           eapply FV_inv_set_r. intros Hc. eapply Hnin.
           subst. now eauto.
@@ -1136,6 +1136,7 @@ Section Closure_conversion_correct.
 
       eapply Hbase.
       eassumption.
+      Unshelve. assumption.
   Qed.
 
 
diff --git a/theories/LambdaANF/closure_conversion_corresp.v b/theories/LambdaANF/closure_conversion_corresp.v
index c6774158..b4b7ad26 100644
--- a/theories/LambdaANF/closure_conversion_corresp.v
+++ b/theories/LambdaANF/closure_conversion_corresp.v
@@ -886,7 +886,7 @@ Section CC_correct.
           rewrite M.gso; eauto. eapply Hget. repeat split; eauto.
           rewrite <- Hnth. now eauto.
         * subst. rewrite Hnth in Hn. eapply nthN_is_Some_length in Hnth.
-          rewrite app_length in Hnth. simpl length in *.
+          rewrite length_app in Hnth. simpl length in *.
           destruct (N - N.of_nat (length FVs))%N eqn:Heq; simpl in Hn; try congruence.
           inv Hn. rewrite M.gss; eauto.
           repeat f_equal. zify. lia. 
@@ -999,7 +999,7 @@ Section CC_correct.
         induction fv as [|v fv IHfv]; intros n vars FVmap_i Hlen Hinv Hb Hb' Hnin Hdis Hdup.
         * simpl. rewrite app_nil_r. eauto.
         * simpl. replace (vars ++ v :: fv) with ((vars ++ [v]) ++ fv). simpl.
-          eapply IHfv. rewrite app_length. simpl. zify. lia.
+          eapply IHfv. rewrite length_app. simpl. zify. lia.
           eapply FVmap_inv_set_free_var. now eauto. eassumption. 
           now intros Hc; inv Hc. now intros Hc; inv Hc. 
           { normalize_sets. apply Disjoint_sym, Disjoint_Union_l in Hdis.
diff --git a/theories/LambdaANF/cps_proto.v b/theories/LambdaANF/cps_proto.v
index 7400df24..93b94659 100644
--- a/theories/LambdaANF/cps_proto.v
+++ b/theories/LambdaANF/cps_proto.v
@@ -626,11 +626,50 @@ Lemma frame_size_gt {A B} (f : exp_frame_t A B) (x : univD A) :
   (univ_size (frameD f x) > univ_size x)%nat.
 Proof.
   destruct f; cbn;
-  try change (size_exp x) with (size x); cbn;
+    try change (size_exp x) with (size x); cbn;
   try change (size_fundefs x) with (size x); cbn;
   try change (size_list (size_prod size size) x) with (size x); cbn;
   try change (size x) with 1; cbn;
   try lia.
+  
+  change ((fix size_exp (e : exp) : nat :=
+            match e with
+            | Ecase _ ces => S (S (size_list (size_prod size size_exp) ces))
+            | Eproj _ _ _ _ e0 => S (S (S (S (S (size_exp e0)))))
+            | Eletapp _ _ _ ys e0 => S (S (S (S (size ys + size_exp e0))))
+            | Efun fds e0 => S (size_fundefs fds + size_exp e0)
+            | Eapp _ _ xs => S (S (S (size xs)))
+            | Eprim_val _ _ e0 => S (S (S (size_exp e0)))
+            | Econstr _ _ ys e0 | Eprim _ _ ys e0 => S (S (S (size ys + size_exp e0)))
+            | Ehalt x0 => S (size x0)
+            end
+            with size_fundefs (fds : fundefs) : nat :=
+              match fds with
+              | Fcons _ _ xs e fds0 => S (S (S (size xs + size_exp e + size_fundefs fds0)))
+              | Fnil => 1
+              end
+                for
+                size_exp) x) with (size x).
+  cbn. lia.
+  change ((fix size_exp (e0 : exp) : nat :=
+             match e0 with
+             | Ecase _ ces => S (S (size_list (size_prod size size_exp) ces))
+             | Eproj _ _ _ _ e1 => S (S (S (S (S (size_exp e1)))))
+             | Eletapp _ _ _ ys e1 => S (S (S (S (size ys + size_exp e1))))
+             | Efun fds e1 => S (size_fundefs fds + size_exp e1)
+             | Eapp _ _ xs => S (S (S (size xs)))
+             | Eprim_val _ _ e1 => S (S (S (size_exp e1)))
+             | Econstr _ _ ys e1 | Eprim _ _ ys e1 => S (S (S (size ys + size_exp e1)))
+             | Ehalt x0 => S (size x0)
+             end
+             with size_fundefs (fds : fundefs) : nat :=
+               match fds with
+               | Fcons _ _ xs e0 fds0 => S (S (S (size xs + size_exp e0 + size_fundefs fds0)))
+               | Fnil => 1
+               end
+                 for
+                 size_fundefs) x) with (size x).
+  cbn. lia.  
 Qed.
 
 Lemma exp_c_size_ge {A B} (C : exp_c A B) (x : univD A) :
diff --git a/theories/LambdaANF/inline_correct.v b/theories/LambdaANF/inline_correct.v
index 4b1dcf8b..560b6713 100644
--- a/theories/LambdaANF/inline_correct.v
+++ b/theories/LambdaANF/inline_correct.v
@@ -1587,7 +1587,7 @@ Section Inline_correct.
               + eapply Union_Disjoint_r. clear H3. now sets. now sets.
               + repeat normalize_bound_var_in_ctx. repeat normalize_occurs_free_in_ctx.
                 eapply Disjoint_Included_r.
-                eapply image_apply_r_set_list. unfold apply_r_list. rewrite map_length. eassumption. 
+                eapply image_apply_r_set_list. unfold apply_r_list. rewrite length_map. eassumption. 
                 eapply Union_Disjoint_r.
                 rewrite FromList_apply_list.
                 eapply Disjoint_Included; [| | eapply Hdis3 ]; [| now sets ]. rewrite !image_Union. now sets.
@@ -1634,7 +1634,7 @@ Section Inline_correct.
                   + eapply Disjoint_Included_r. eapply Singleton_Included. eassumption. sets.
                   + eapply Disjoint_Included_r. eapply Included_trans. eapply Singleton_Included. eassumption.
                     eassumption.
-                    eapply Disjoint_Included_r. eapply image_apply_r_set_list. unfold apply_r_list. rewrite map_length. now eauto.
+                    eapply Disjoint_Included_r. eapply image_apply_r_set_list. unfold apply_r_list. rewrite length_map. now eauto.
                     rewrite !Setminus_Union_distr, image_Union.
                     eapply Union_Disjoint_r; [| eapply Union_Disjoint_r ].
                     rewrite FromList_apply_list. eapply Disjoint_Included; [| | eapply Hdis3 ]; now sets.
@@ -1694,7 +1694,7 @@ Section Inline_correct.
                     sets. }
                   eapply Included_trans. eassumption. eapply Union_Included.
                   -- eapply Included_trans. eassumption. eapply Included_trans.
-                     eapply image_apply_r_set_list. unfold apply_r_list. rewrite map_length. eassumption.
+                     eapply image_apply_r_set_list. unfold apply_r_list. rewrite length_map. eassumption.
                      normalize_occurs_free. rewrite Setminus_Union_distr, !image_Union. eapply Union_Included.
                      rewrite FromList_apply_list. now sets.
                      eapply Union_Included. eapply Included_trans.
diff --git a/theories/LambdaANF/lambda_lifting_correct.v b/theories/LambdaANF/lambda_lifting_correct.v
index dea89178..2bc48c56 100644
--- a/theories/LambdaANF/lambda_lifting_correct.v
+++ b/theories/LambdaANF/lambda_lifting_correct.v
@@ -322,8 +322,8 @@ Section Lambda_lifting_correct.
         rewrite list_length_map. lia.
 
         eapply preord_exp_app_r with (P1 := P1 1); [|  | | eassumption | | ].
-        * rewrite <- (map_length f1 fvs). rewrite Hleq. 
-          rewrite <- app_length.  eapply P1_local_app'. 
+        * rewrite <- (length_map f1 fvs). rewrite Hleq. 
+          rewrite <- length_app.  eapply P1_local_app'. 
         * assert (Hfeq'' : f2 f' = f'). {
             erewrite <- Make_wrappers_f_eq_subdomain with (Q := [set f']); [| eassumption | | reflexivity ].
             2:{ eapply Disjoint_Included; [| | eapply Hdis' ]; sets. }
@@ -574,7 +574,7 @@ Section Lambda_lifting_correct.
         destruct Ha as [vfvs Hgetfvs].
         
         assert (Hfset : exists rho2', set_lists (xs1 ++ ys) (vs2 ++ vfvs) (def_funs B2 B2 rho' rho') = Some rho2').
-        { eapply set_lists_length3. rewrite !app_length, Hleq1.
+        { eapply set_lists_length3. rewrite !length_app, Hleq1.
           eapply get_list_length_eq in Hgetfvs. rewrite list_length_map in Hgetfvs.
           symmetry in Hset. eapply set_lists_length_eq in Hset. rewrite Hgetfvs, <- Hleq. f_equal. eassumption. }
         destruct Hfset as [rho2' Hsetapp].
@@ -617,7 +617,7 @@ Section Lambda_lifting_correct.
                  eapply Make_wrappers_image_Included. eassumption.
                  eapply Union_Disjoint_l.
                  + eapply Disjoint_Included_l. eapply image_extend_lst_Included.
-                   rewrite !app_length. rewrite Hleq1. reflexivity.
+                   rewrite !length_app. rewrite Hleq1. reflexivity.
                    rewrite !FromList_app. eapply Union_Disjoint_l.
                    * rewrite <- Setminus_Union. eapply Disjoint_Included; [| | eapply Himdis ].
                      eapply Included_Union_compat; [| now sets ]. eapply Included_trans. eapply Hssub. eassumption.
@@ -653,7 +653,7 @@ Section Lambda_lifting_correct.
                  rewrite <- Make_wrapper_image; [| eassumption | now sets ]. 
 
                  eapply binding_in_map_antimon.
-                 eapply image_extend_lst_Included. rewrite !app_length. rewrite <- Hleq1. reflexivity.
+                 eapply image_extend_lst_Included. rewrite !length_app. rewrite <- Hleq1. reflexivity.
                  rewrite Union_commut. eapply binding_in_map_set_lists; [| eassumption ]. 
                  rewrite FromList_app. rewrite <- Setminus_Union.
 
@@ -693,7 +693,7 @@ Section Lambda_lifting_correct.
                        * eapply Disjoint_Included_l. eassumption. eapply Disjoint_Included_r. eassumption.
                          eapply Disjoint_Included; [| | eapply Hd2 ]; sets. eapply Included_trans; eassumption.
                    - rewrite extend_lst_app.  eassumption. reflexivity.
-                   - eapply Disjoint_Included_l. eapply image_extend_lst_Included. rewrite !app_length. congruence.
+                   - eapply Disjoint_Included_l. eapply image_extend_lst_Included. rewrite !length_app. congruence.
                      rewrite !FromList_app. eapply Union_Disjoint_l.
                      + eapply Disjoint_Included; [| | eapply Himdis ].
                        eapply Included_trans. eassumption. eapply Included_trans. eapply Included_trans. eapply Setminus_Included.
@@ -715,7 +715,7 @@ Section Lambda_lifting_correct.
                - eapply Make_wrappers_Funs_inv. eassumption. rewrite extend_lst_app. eassumption. reflexivity.
                  now xsets.
                  eapply Disjoint_Included_r. eapply Included_trans. eapply Setminus_Included. eassumption.
-                 eapply Disjoint_Included_l. eapply image_extend_lst_Included. rewrite !app_length. congruence.
+                 eapply Disjoint_Included_l. eapply image_extend_lst_Included. rewrite !length_app. congruence.
                  rewrite !FromList_app. eapply Union_Disjoint_l.
                  + eapply Disjoint_Included; [| | eapply Himdis ].
                    eapply Setminus_Included_Included_Union. eapply Included_trans. eassumption. now sets.
diff --git a/theories/LambdaANF/lambda_lifting_util.v b/theories/LambdaANF/lambda_lifting_util.v
index 21e86da1..c4384bb6 100644
--- a/theories/LambdaANF/lambda_lifting_util.v
+++ b/theories/LambdaANF/lambda_lifting_util.v
@@ -1603,7 +1603,7 @@ Proof with now eauto with Ensembles_DB.
       eapply Make_wrappers_occurs_free. eassumption. reflexivity.
       rewrite Setminus_Union_distr. eapply Union_Included.
       * eapply Included_trans. eapply Included_Setminus_compat.
-        eapply image_extend_lst_Included. rewrite !app_length.
+        eapply image_extend_lst_Included. rewrite !length_app.
         rewrite H24. reflexivity. reflexivity. repeat normalize_sets.
         apply Included_Union_preserv_l.
         rewrite !image_Union, !Setminus_Union_distr.
@@ -1633,7 +1633,7 @@ Proof with now eauto with Ensembles_DB.
         rewrite <- Make_wrapper_image; eauto; sets. 
         eapply Union_Disjoint_l.
         eapply Disjoint_Included_l.
-        eapply image_extend_lst_Included. rewrite !app_length. rewrite H24. reflexivity.
+        eapply image_extend_lst_Included. rewrite !length_app. rewrite H24. reflexivity.
         repeat normalize_sets.  
         rewrite !Setminus_Union. rewrite !Setminus_Union_distr.
         eapply Union_Disjoint_l.
@@ -1724,7 +1724,7 @@ Proof with now eauto with Ensembles_DB.
            { rewrite <- Make_wrapper_image; eauto. 2: eauto with Ensembles_DB.
              subst Dom; rewrite !Setminus_Union_distr.
              eapply Included_trans. eapply Included_Setminus_compat.
-             eapply image_extend_lst_Included. rewrite !app_length.
+             eapply image_extend_lst_Included. rewrite !length_app.
              rewrite H24. reflexivity. reflexivity. repeat normalize_sets.
              eapply Included_Union_preserv_l.
              repeat rewrite !Setminus_Union_distr, !Setminus_Union.
@@ -2382,7 +2382,7 @@ Proof with now eauto with Ensembles_DB.
         simpl. rewrite image'_Union, image'_Singleton_is_Some.
         2:{ eapply lifted_name_eq. eassumption. }
         now left.
-    + eapply NoDup_app; eauto.
+    + eapply List_util.NoDup_app; eauto.
       eapply Disjoint_Included_r. eassumption. sets.
     + constructor.
       eapply IHe; eauto. repeat find_subsets; sets.
diff --git a/theories/LambdaANF/set_util.v b/theories/LambdaANF/set_util.v
index eaca86a2..9a94d743 100644
--- a/theories/LambdaANF/set_util.v
+++ b/theories/LambdaANF/set_util.v
@@ -954,7 +954,7 @@ Proof.
   intros Hd.
   rewrite !PS.cardinal_spec.
   erewrite (@Permutation_length _ (PS.elements (PS.union s1 s2))).
-  rewrite <- app_length. reflexivity.
+  rewrite <- length_app. reflexivity.
   symmetry. eapply PS_union_elements. eassumption.
 Qed.
 
diff --git a/theories/LambdaANF/size_cps.v b/theories/LambdaANF/size_cps.v
index d22ef4e8..28813547 100644
--- a/theories/LambdaANF/size_cps.v
+++ b/theories/LambdaANF/size_cps.v
@@ -444,7 +444,7 @@ Proof.
     eassumption.
     rewrite <- HP in Hnd.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite app_length.
+    rewrite length_app.
     eapply (Included_trans (FromList l2) (Setminus var (occurs_free e) [set v])) in Hin2;
       [| now apply Setminus_Included ].
     eapply Same_set_FromList_length in Hin1.
@@ -460,7 +460,7 @@ Proof.
     eassumption.
     rewrite <- HP in Hnd.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite !app_length.
+    rewrite !length_app.
     eapply IHe in Hin1. eapply IHl in Hin2. simpl in *. lia.
     eapply NoDup_cons_r; eauto. 
     eapply NoDup_cons_l; eauto.
@@ -469,7 +469,7 @@ Proof.
     eassumption.
     rewrite <- HP in Hnd.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite app_length.
+    rewrite length_app.
     eapply (Included_trans (FromList l2) (Setminus var (occurs_free e) [set v])) in Hin2;
       [| now apply Setminus_Included ].
     rewrite <- (Union_Empty_set_neut_r [set v0]) in Hin1.
@@ -482,7 +482,7 @@ Proof.
     eassumption.
     rewrite <- HP in Hnd.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite app_length.
+    rewrite length_app.
     eapply (Included_trans (FromList l2) (Setminus var (occurs_free e) [set x])) in Hin2;
       [| now apply Setminus_Included ].
     rewrite <- FromList_cons in Hin1.
@@ -494,7 +494,7 @@ Proof.
     eassumption.
     rewrite <- HP in Hnd.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite app_length.
+    rewrite length_app.
     eapply (Included_trans (FromList l2) (Setminus var (occurs_free e) _)) in Hin2;
       [| now apply Setminus_Included ].
     eapply IHb in Hin1. eapply IHe in Hin2. lia.
@@ -504,7 +504,7 @@ Proof.
     eassumption. rewrite <- HP in Hnd.
     eapply Same_set_FromList_length in Hin1; eauto.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite app_length.
+    rewrite length_app.
     rewrite <- (Union_Empty_set_neut_r [set v]) in Hin2.
     rewrite <- FromList_nil, <- FromList_cons in Hin2.
     eapply Same_set_FromList_length in Hin2.
@@ -519,7 +519,7 @@ Proof.
     eassumption.
     rewrite <- HP in Hnd.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite app_length.
+    rewrite length_app.
     eapply (Included_trans (FromList l2) (Setminus var (occurs_free e) [set v])) in Hin2;
       [| now apply Setminus_Included ].
     eapply Same_set_FromList_length in Hin1.
@@ -532,7 +532,7 @@ Proof.
   - edestruct (@FromList_Union_split var) as [l1 [l2 [HP [Hin1 Hin2]]]].
     eassumption. rewrite <- HP in Hnd.
     eapply Permutation_length in HP. rewrite <- HP.
-    rewrite app_length.
+    rewrite length_app.
     eapply (Included_trans (FromList l2) (Setminus var _ [set v])) in Hin2;
       [| now apply Setminus_Included ].
     eapply (Included_trans (FromList l1) (Setminus var _ _)) in Hin1;
diff --git a/theories/LambdaANF/uncurry_correct.v b/theories/LambdaANF/uncurry_correct.v
index fe3e1625..33f78bf4 100644
--- a/theories/LambdaANF/uncurry_correct.v
+++ b/theories/LambdaANF/uncurry_correct.v
@@ -467,7 +467,7 @@ Section uncurry_correct.
           eapply length_exists_set_lists in Hrho1''; destruct Hrho1'' as [rho1'' Hrho1''].
           do 3 eexists; split; [reflexivity|split]; [eassumption|intros Hk2 Hvs3_vs4].
           assert (Hrho''' : length (gv ++ fv) = length (vs4 ++ tvs2)). {
-            do 2 rewrite app_length.
+            do 2 rewrite length_app.
             apply set_lists_length in Hrho1''.
             rewrite <- Hrho1''.
             rewrite <- Hgv_gv1.
@@ -1123,7 +1123,7 @@ Section uncurry_correct.
         do 3 eexists; split; [reflexivity|split]; [eassumption|intros Hk2 Hvs3_vs4].
         rename xs1 into fv.
         assert (Hrho''' : length (gv ++ fv) = length (vs4 ++ tvs2)). {
-          do 2 rewrite app_length.
+          do 2 rewrite length_app.
           apply set_lists_length in Hrho1''.
           rewrite <- Hrho1''.
           rewrite <- Hgv_gv1.
diff --git a/theories/LambdaANF/uncurry_proto.v b/theories/LambdaANF/uncurry_proto.v
index f4ece88c..3beeeb07 100644
--- a/theories/LambdaANF/uncurry_proto.v
+++ b/theories/LambdaANF/uncurry_proto.v
@@ -307,6 +307,44 @@ Proof.
   - cbn in *; subst fds'0. decompose [and] H; subst fds'; cbn; intros _.
     assert (size (gv ++ fv) < size gv + size fv) by now apply size_app.
     lia.
+  - cbn in *.
+    change ((fix size_exp (e1 : exp) : nat :=
+               match e1 with
+               | Ecase _ ces => S (S (size_list (size_prod size size_exp) ces))
+               | Eproj _ _ _ _ e2 => S (S (S (S (S (size_exp e2)))))
+               | Eletapp _ _ _ ys e2 => S (S (S (S (size ys + size_exp e2))))
+               | Efun fds e2 => S (size_fundefs fds + size_exp e2)
+               | Eapp _ _ xs => S (S (S (size xs)))
+               | Eprim_val _ _ e2 => S (S (S (size_exp e2)))
+               | Econstr _ _ ys e2 | Eprim _ _ ys e2 => S (S (S (size ys + size_exp e2)))
+               | Ehalt x => S (size x)
+               end
+               with size_fundefs (fds : fundefs) : nat :=
+                 match fds with
+                 | Fcons _ _ xs e1 fds0 => S (S (S (size xs + size_exp e1 + size_fundefs fds0)))
+                 | Fnil => 1
+                 end
+                   for
+                   size_exp) e0) with (size e0). cbn. lia.
+  - cbn in *.
+    change ((fix size_exp (e1 : exp) : nat :=
+               match e1 with
+               | Ecase _ ces => S (S (size_list (size_prod size size_exp) ces))
+               | Eproj _ _ _ _ e2 => S (S (S (S (S (size_exp e2)))))
+               | Eletapp _ _ _ ys e2 => S (S (S (S (size ys + size_exp e2))))
+               | Efun fds e2 => S (size_fundefs fds + size_exp e2)
+               | Eapp _ _ xs => S (S (S (size xs)))
+               | Eprim_val _ _ e2 => S (S (S (size_exp e2)))
+               | Econstr _ _ ys e2 | Eprim _ _ ys e2 => S (S (S (size ys + size_exp e2)))
+               | Ehalt x => S (size x)
+               end
+               with size_fundefs (fds : fundefs) : nat :=
+                 match fds with
+                 | Fcons _ _ xs e1 fds0 => S (S (S (size xs + size_exp e1 + size_fundefs fds0)))
+                 | Fnil => 1
+                 end
+                   for
+                   size_fundefs) f) with (size f). cbn. lia.
 Defined.
 
 Set Extraction Flag 2031. (* default + linear let + linear beta *)
diff --git a/theories/LambdaANF/uncurry_rel.v b/theories/LambdaANF/uncurry_rel.v
index dd4f2350..c736aed2 100644
--- a/theories/LambdaANF/uncurry_rel.v
+++ b/theories/LambdaANF/uncurry_rel.v
@@ -89,11 +89,11 @@ Section list_lemmas.
       + rewrite <- IHl in Heqo0. rewrite <- Heqo in Heqo0. inversion Heqo0; now subst.
       + apply set_lists_length in Heqo.
         assert (length (l ++ [a]) = length (v ++ [b]))
-          by (repeat rewrite app_length; now rewrite Heqo).
+          by (repeat rewrite length_app; now rewrite Heqo).
         apply @length_exists_set_lists with (rho := rho) in H. destruct H. congruence.
       + assert (length l = length v). {
           apply set_lists_length in Heqo0. 
-          repeat rewrite app_length in Heqo0. simpl in Heqo0. lia.
+          repeat rewrite length_app in Heqo0. simpl in Heqo0. lia.
         }
         apply @length_exists_set_lists with (rho := (M.set a b rho)) in H. destruct H. congruence.
   Qed.
@@ -106,7 +106,7 @@ Section list_lemmas.
     length l = length (a ++ [b]) -> exists a1 b1, l = a1 ++ [b1].
   Proof.
     induction l; intros.
-    - rewrite app_length in H. inversion H. rewrite Nat.add_comm in H1. inversion H1.
+    - rewrite length_app in H. inversion H. rewrite Nat.add_comm in H1. inversion H1.
     - destruct a0.
       + assert (l = []) by (destruct l; [easy|inversion H]). subst.
         now exists [], a.
@@ -1331,7 +1331,7 @@ Proof with eauto with Ensembles_DB.
       intros contra; rewrite FromList_app in contra; destruct contra.
       contradiction H6; apply H8; do 4 left; now right.
       contradiction H6; apply H8; do 6 left; right; now right.
-      apply NoDup_app.
+      apply List_util.NoDup_app.
       inv H9. inv H26. now inv H16.
       inv H9. now inv H25.
       constructor; intros a contra; inv contra.
@@ -1377,7 +1377,7 @@ Proof with eauto with Ensembles_DB.
     | |- Disjoint _ (_ :|: _) _ => apply Union_Disjoint_l
     | |- Disjoint _ _ (_ :|: _) => apply Union_Disjoint_r
     | |- ~ In _ (_ :|: _) _ => rewrite Union_demorgan; split
-    | |- NoDup (_ ++ _) => apply NoDup_app
+    | |- NoDup (_ ++ _) => apply List_util.NoDup_app
     end...
     + intros Hin. apply (Disjoint_In_falso _ _ Hin)...
     + now apply Disjoint_sym.
diff --git a/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v b/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v
index 28407722..4833e93f 100644
--- a/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v
+++ b/theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v
@@ -1197,7 +1197,7 @@ Proof.
     rewrite (proj1 (closed_subst_sbst _ H0)).
     rewrite sbst_lets.
     eapply IHk; eauto.
-    rewrite sbst_env_length, app_length; simpl; lia.
+    rewrite sbst_env_length, length_app; simpl; lia.
     rewrite subst_env_app in H1. simpl in H1.
     rewrite <- wf_tr_environ_sbst in H1; auto.
     unfold sbst_env in H1 |- *.
diff --git a/theories/LambdaBoxLocal/fuel_sem.v b/theories/LambdaBoxLocal/fuel_sem.v
index af424b40..475ed0db 100644
--- a/theories/LambdaBoxLocal/fuel_sem.v
+++ b/theories/LambdaBoxLocal/fuel_sem.v
@@ -274,8 +274,8 @@ Section FUEL_SEM.
       intros e e' bs rho i d vs f t Heval Hwf H.
       inv Hwf.
       unfold well_formed_in_env.
-      rewrite app_length. rewrite Nnat.Nat2N.inj_add.
-      rewrite rev_length. eapply find_branch_preserves_wf; eassumption.
+      rewrite length_app. rewrite Nnat.Nat2N.inj_add.
+      rewrite length_rev. eapply find_branch_preserves_wf; eassumption.
     Qed.
 
     Lemma well_formed_envmake_rec_env_rev_order fnlst rho rho' : 
@@ -378,7 +378,7 @@ Section FUEL_SEM.
           with (1 + N.of_nat (Datatypes.length (make_rec_env_rev_order fnlst rho'))) by lia.
 
         edestruct make_rec_env_rev_order_app. destructAll. rewrite H2.
-        rewrite app_length. rewrite Nnat.Nat2N.inj_add.
+        rewrite length_app. rewrite Nnat.Nat2N.inj_add.
         rewrite H7. rewrite efnlength_efnlst_length. eassumption. 
 
       - subst. 
diff --git a/theories/LambdaBoxMut/compile.v b/theories/LambdaBoxMut/compile.v
index f83ea6f9..755480bc 100644
--- a/theories/LambdaBoxMut/compile.v
+++ b/theories/LambdaBoxMut/compile.v
@@ -340,6 +340,7 @@ Fixpoint list_Defs (l : list (def Term)) : Defs :=
 Polymorphic Equations trans_prim_val {T} (p : EPrimitive.prim_val T) : option primitive :=
   trans_prim_val (existT _ primInt (primIntModel i)) => Some (existT _ AstCommon.primInt i) ;
   trans_prim_val (existT _ primFloat (primFloatModel i)) => Some (existT _ AstCommon.primFloat i) ;
+  trans_prim_val (existT _ primString _) => None ;
   trans_prim_val (existT _ primArray _) => None.
 
 Section LiftSize.
diff --git a/theories/LambdaBoxMut/stripEvalCommute.v b/theories/LambdaBoxMut/stripEvalCommute.v
index 5da241b7..cecace67 100644
--- a/theories/LambdaBoxMut/stripEvalCommute.v
+++ b/theories/LambdaBoxMut/stripEvalCommute.v
@@ -30,9 +30,10 @@ Local Open Scope list.
 Set Implicit Arguments.
 
 (** We do not support arrays (yet) *)
-Definition prim_flags := 
-  {| has_primint := true;   
+Definition prim_flags :=
+  {| has_primint := true;
      has_primfloat := true;
+     has_primstring := false ;
      has_primarray := false |}.
 
 (** Cofixpoints are not supported, Var and Evar don't actually appear 
@@ -552,7 +553,7 @@ Proof.
     eapply compile_crctInd; tea. eauto.
     repeat toAll. clear -wfΣ crctΣ H1.
     induction H1; cbn; constructor; auto.
-    rewrite List.rev_length. now apply p. 
+    rewrite List.length_rev. now apply p. 
   - cbn. rewrite -dlength_hom. 
     move/andP: H0 => [] hn H1. clear hn.
     rewrite Nat.add_comm. eapply forallb_All in H1. eapply forallb_All in H.
@@ -563,7 +564,9 @@ Proof.
     constructor; eauto.
     now eapply compile_isLambda.
   - cbn. rewrite -dlength_hom. move/andP: H0 => [] /Nat.ltb_lt //.
-  - destruct p as [? []]; try constructor; eauto. simp trans_prim_val. cbn. now cbn in H.
+  - destruct p as [? []]; try constructor; eauto.
+    + simp trans_prim_val. cbn. now cbn in H.
+    + simp trans_prim_val. cbn. now cbn in H.
   - specialize (H k H0). now eapply Crct_lift in H.
 Qed.
 
@@ -806,7 +809,7 @@ Proof.
     { subst brs' brs'0. repeat toAll. induction wfl.
     - constructor.
     - cbn -[instantiateBrs]. rewrite instantiateBrs_equation.
-      f_equal; eauto. destruct p. rewrite List.rev_length. repeat eapply (e n).
+      f_equal; eauto. destruct p. rewrite List.length_rev. repeat eapply (e n).
       eapply wellformed_up; tea. lia. }
   - rewrite map_map_compose. set (mfix' := map _ m).
     simpl. (*rewrite instantiate_TFix. *) f_equal.
@@ -1063,7 +1066,7 @@ Proof.
     subst pars. rewrite skipn_0 in hbr.
     econstructor; tea.
     unfold whCaseStep.
-    rewrite (nth_error_bnth hnth) List.rev_length tlength_hom.
+    rewrite (nth_error_bnth hnth) List.length_rev tlength_hom.
     case: Nat.eqb_spec => //; try congruence.
     intros _. rewrite /iota_red skipn_0.
     f_equal. rewrite (compile_substl (Σ := Σ)) //. solve_all.
diff --git a/theories/common/RandyPrelude.v b/theories/common/RandyPrelude.v
index f9591fd6..e2c219a2 100644
--- a/theories/common/RandyPrelude.v
+++ b/theories/common/RandyPrelude.v
@@ -423,7 +423,7 @@ Qed.
 Lemma list_to_n_length:
   forall m, List.length (list_to_n m) = m.
 Proof.
-  intros. unfold list_to_n. rewrite rev_length. apply list_to_zero_length.
+  intros. unfold list_to_n. rewrite length_rev. apply list_to_zero_length.
 Qed.
 
 Lemma list_to_n_S: