diff --git a/common/theories/Environment.v b/common/theories/Environment.v
index 6ae92df47..9d3ca8ece 100644
--- a/common/theories/Environment.v
+++ b/common/theories/Environment.v
@@ -42,25 +42,28 @@ Module Retroknowledge.
   Record t := mk_retroknowledge {
     retro_int63 : option kername;
     retro_float64 : option kername;
+    retro_string : option kername;
     retro_array : option kername;
   }.
 
-  Definition empty := {| retro_int63 := None; retro_float64 := None; retro_array := None |}.
+  Definition empty := {| retro_int63 := None; retro_float64 := None; retro_string := None; retro_array := None |}.
 
   Definition extends (x y : t) :=
     option_extends x.(retro_int63) y.(retro_int63) /\
     option_extends x.(retro_float64) y.(retro_float64) /\
+    option_extends x.(retro_string) y.(retro_string) /\
     option_extends x.(retro_array) y.(retro_array).
   Existing Class extends.
 
   Definition extendsb (x y : t) :=
     option_extendsb x.(retro_int63) y.(retro_int63) &&
     option_extendsb x.(retro_float64) y.(retro_float64) &&
-    option_extendsb x.(retro_array) y.(retro_array).
+    option_extendsb x.(retro_string) y.(retro_string) &&
+      option_extendsb x.(retro_array) y.(retro_array).
 
   Lemma extendsT x y : reflect (extends x y) (extendsb x y).
   Proof.
-    rewrite /extends/extendsb; do 3 case: option_extendsT; cbn; constructor; intuition auto.
+    rewrite /extends/extendsb; do 4 case: option_extendsT; cbn; constructor; intuition auto.
   Qed.
 
   Lemma extends_spec x y : extendsb x y <-> extends x y.
@@ -76,22 +79,24 @@ Module Retroknowledge.
 
   #[global] Instance extends_trans : RelationClasses.Transitive Retroknowledge.extends.
   Proof.
-    intros x y z [? []] [? []]; repeat split; cbn; now etransitivity; tea.
+    intros x y z [? [? []]] [? [? []]]; repeat split; cbn; now etransitivity; tea.
   Qed.
 
   #[export,program] Instance reflect_t : ReflectEq t := {
       eqb x y := (x.(retro_int63) == y.(retro_int63)) &&
                  (x.(retro_float64) == y.(retro_float64)) &&
+                 (x.(retro_string) == y.(retro_string)) &&
                  (x.(retro_array) == y.(retro_array))
     }.
   Next Obligation.
-    do 3 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence.
+    do 4 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence.
   Qed.
 
   (** This operation is asymmetric; it perfers the first argument when the arguments are incompatible, but otherwise takes the join *)
   Definition merge (r1 r2 : t) : t
     := {| retro_int63 := match r1.(retro_int63) with Some v => Some v | None => r2.(retro_int63) end
        ; retro_float64 := match r1.(retro_float64) with Some v => Some v | None => r2.(retro_float64) end
+       ; retro_string := match r1.(retro_string) with Some v => Some v | None => r2.(retro_string) end
        ; retro_array := match r1.(retro_array) with Some v => Some v | None => r2.(retro_array) end
         |}.
 
@@ -112,6 +117,7 @@ Module Retroknowledge.
   Definition compatible (x y : t) : bool
     := match x.(retro_int63), y.(retro_int63) with Some x, Some y => x == y | _, _ => true end
        && match x.(retro_float64), y.(retro_float64) with Some x, Some y => x == y | _, _ => true end
+       && match x.(retro_string), y.(retro_string) with Some x, Some y => x == y | _, _ => true end
        && match x.(retro_array), y.(retro_array) with Some x, Some y => x == y | _, _ => true end.
 
   Lemma extends_r_merge r1 r2
@@ -846,6 +852,7 @@ Module Environment (T : Term).
     match p with
     | primInt => Σ.(retroknowledge).(Retroknowledge.retro_int63)
     | primFloat => Σ.(retroknowledge).(Retroknowledge.retro_float64)
+    | primString => Σ.(retroknowledge).(Retroknowledge.retro_string)
     | primArray => Σ.(retroknowledge).(Retroknowledge.retro_array)
     end.
 
@@ -857,7 +864,7 @@ Module Environment (T : Term).
 
   Definition primitive_invariants (p : prim_tag) (cdecl : constant_body) :=
     match p with
-    | primInt | primFloat =>
+    | primInt | primFloat | primString =>
      [/\ cdecl.(cst_type) = tSort Sort.type0, cdecl.(cst_body) = None &
           cdecl.(cst_universes) = Monomorphic_ctx]
     | primArray =>
diff --git a/common/theories/Primitive.v b/common/theories/Primitive.v
index f8283f6fc..278f9d056 100644
--- a/common/theories/Primitive.v
+++ b/common/theories/Primitive.v
@@ -7,5 +7,6 @@ Local Open Scope bs.
 Variant prim_tag :=
   | primInt
   | primFloat
+  | primString
   | primArray.
 Derive NoConfusion EqDec for prim_tag.
diff --git a/erasure/theories/EArities.v b/erasure/theories/EArities.v
index f80d881f6..052269c0e 100644
--- a/erasure/theories/EArities.v
+++ b/erasure/theories/EArities.v
@@ -1010,13 +1010,14 @@ Proof.
   destruct p as [? []]; simp prim_type.
   - eexists [], []. reflexivity.
   - eexists [], []; reflexivity.
+  - eexists [], []; reflexivity.
   - eexists [_], [_]; reflexivity.
 Qed.
 
 Lemma primitive_invariants_axiom t decl : primitive_invariants t decl -> cst_body decl = None.
 Proof.
   destruct t; cbn => //.
-  1-2:now intros [? []].
+  1-3:now intros [? []].
   now intros [].
 Qed.
 
@@ -1052,6 +1053,13 @@ Proof.
       rewrite hd in hs'. cbn in hs'.
       eapply ws_cumul_pb_Sort_inv in hs'. red in hs'.
       destruct s => //.
+    * destruct p0 as [hd hb hu].
+      eapply inversion_Const in hs as [decl' [wf [decl'' [cu hs']]]]; eauto.
+      unshelve eapply declared_constant_to_gen in d, decl''. 3,6:eapply wfΣ.
+      eapply declared_constant_inj in d; tea. subst decl'.
+      rewrite hd in hs'. cbn in hs'.
+      eapply ws_cumul_pb_Sort_inv in hs'. red in hs'.
+      destruct s => //.
     * destruct p0 as [hd hb hu].
       eapply inversion_App in hs as [na [A [B [hp [harg hres]]]]]; eauto.
       eapply inversion_Const in hp as [decl' [wf [decl'' [cu hs']]]]; eauto.
@@ -1064,4 +1072,4 @@ Proof.
       pose proof (ws_cumul_pb_trans _ _ _ w1 hres) as X0.
       eapply ws_cumul_pb_Sort_inv in X0.
       destruct s => //.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/erasure/theories/EAstUtils.v b/erasure/theories/EAstUtils.v
index de7c2655c..2058db50c 100644
--- a/erasure/theories/EAstUtils.v
+++ b/erasure/theories/EAstUtils.v
@@ -386,6 +386,7 @@ Section PrimDeps.
   Equations prim_global_deps (p : prim_val term) : KernameSet.t :=
    | (primInt; primIntModel i) => KernameSet.empty
    | (primFloat; primFloatModel f) => KernameSet.empty
+   | (primString; primStringModel s) => KernameSet.empty
    | (primArray; primArrayModel a) =>
       List.fold_left (fun acc x => KernameSet.union (deps x) acc) a.(array_value) (deps a.(array_default)).
 
@@ -414,4 +415,4 @@ Fixpoint term_global_deps (t : term) :=
   | tLazy t => term_global_deps t
   | tForce t => term_global_deps t
   | _ => KernameSet.empty
-  end.
\ No newline at end of file
+  end.
diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v
index b1180b5cc..9f6c273d8 100644
--- a/erasure/theories/EDeps.v
+++ b/erasure/theories/EDeps.v
@@ -455,6 +455,7 @@ Proof.
     constructor; [now apply f|now apply f'].
   - eapply Hprim; tea; constructor.
   - eapply Hprim; tea; constructor.
+  - eapply Hprim; tea; constructor.
   - eapply Hprim; tea; constructor.
     intuition auto; solve_all.
     split. auto. destruct a as [d v]. cbn in *.
diff --git a/erasure/theories/EInduction.v b/erasure/theories/EInduction.v
index 53d4d9bc0..a399afa00 100644
--- a/erasure/theories/EInduction.v
+++ b/erasure/theories/EInduction.v
@@ -101,6 +101,7 @@ Definition prim_size (f : term -> nat) (p : prim_val term) : nat :=
   match p.π2 with
   | primIntModel _ => 0
   | primFloatModel _ => 0
+  | primStringModel _ => 0
   | primArrayModel a => f a.(array_default) + list_size f a.(array_value)
   end.
 
@@ -404,4 +405,4 @@ Proof.
     | _ => 1
     end.
 
-End TermSpineView.*)
\ No newline at end of file
+End TermSpineView.*)
diff --git a/erasure/theories/EPretty.v b/erasure/theories/EPretty.v
index 9c99f2e64..c5016220b 100644
--- a/erasure/theories/EPretty.v
+++ b/erasure/theories/EPretty.v
@@ -88,6 +88,7 @@ Module PrintTermTree.
       match p.π2 return Tree.t with
       | primIntModel f => "(int: " ^ show f ^ ")"
       | primFloatModel f => "(float: " ^ show f ^ ")"
+      | primStringModel f => "(string: " ^ show f ^ ")"
       | primArrayModel a => "(array:" ^ soft a.(array_default) ^ " , " ^ string_of_list soft a.(array_value) ^ ")"
       end.
 
diff --git a/erasure/theories/EPrimitive.v b/erasure/theories/EPrimitive.v
index 769949f18..658f1293f 100644
--- a/erasure/theories/EPrimitive.v
+++ b/erasure/theories/EPrimitive.v
@@ -30,6 +30,7 @@ Section PrimModel.
   Inductive prim_model : prim_tag -> Type@{i} :=
   | primIntModel (i : PrimInt63.int) : prim_model primInt
   | primFloatModel (f : PrimFloat.float) : prim_model primFloat
+  | primStringModel (s : PrimString.string) : prim_model primString
   | primArrayModel (a : array_model) : prim_model primArray.
 
   Derive Signature NoConfusion NoConfusionHom for prim_model.
@@ -38,6 +39,7 @@ Section PrimModel.
     match p with
     | primInt => PrimInt63.int
     | primFloat => PrimFloat.float
+    | primString => PrimString.string
     | primArray => array_model
     end.
 
@@ -47,12 +49,14 @@ Section PrimModel.
 
   Definition prim_int i : prim_val := (primInt; primIntModel i).
   Definition prim_float f : prim_val := (primFloat; primFloatModel f).
+  Definition prim_string s : prim_val := (primString; primStringModel s).
   Definition prim_array a : prim_val := (primArray; primArrayModel a).
 
   Definition prim_model_val (p : prim_val) : prim_model_of (prim_val_tag p) :=
     match prim_val_model p in prim_model t return prim_model_of t with
     | primIntModel i => i
     | primFloatModel f => f
+    | primStringModel s => s
     | primArrayModel a => a
     end.
 
@@ -85,9 +89,23 @@ Section PrimModel.
     all:constructor; congruence.
   Qed.
 
+  #[program,global]
+  Instance reflect_eq_pstring : ReflectEq PrimString.string :=
+    { eqb := (fun s1 s2 => match PrimString.compare s1 s2 with Eq => true | _ => false end) }.
+  Next Obligation. discriminate. Qed.
+  Next Obligation. discriminate. Qed.
+  Next Obligation.
+    intros s1 s2. simpl.
+    destruct (PrimString.compare s1 s2) eqn:Hcmp; constructor.
+    - by apply PString.string_eq_spec in Hcmp.
+    - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp.
+    - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp.
+  Qed.
+
   Equations eqb_prim_model {req : term -> term -> bool} {t : prim_tag} (x y : prim_model t) : bool :=
     | primIntModel x, primIntModel y := ReflectEq.eqb x y
     | primFloatModel x, primFloatModel y := ReflectEq.eqb x y
+    | primStringModel x, primStringModel y := ReflectEq.eqb x y
     | primArrayModel x, primArrayModel y := eqb_array (eqt:=req) x y.
 
   #[global, program]
@@ -97,6 +115,7 @@ Section PrimModel.
     intros. depelim x; depelim y; simp eqb_prim_model.
     case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
     case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
+    case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
     change (eqb_array a a0) with (eqb a a0).
     case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
   Qed.
@@ -107,6 +126,7 @@ Section PrimModel.
   Equations eqb_prim_val {req : term -> term -> bool} (x y : prim_val) : bool :=
     | (primInt; i), (primInt; i') := eqb_prim_model (req := req) i i'
     | (primFloat; f), (primFloat; f') := eqb_prim_model (req := req) f f'
+    | (primString; s), (primString; s') := eqb_prim_model (req := req) s s'
     | (primArray; a), (primArray; a') := eqb_prim_model (req := req) a a'
     | x, y := false.
 
@@ -115,22 +135,19 @@ Section PrimModel.
     {| ReflectEq.eqb := eqb_prim_val (req := eqb) |}.
   Next Obligation.
     intros. funelim (eqb_prim_val x y); simp eqb_prim_val.
-    change (eqb_prim_model i i') with (eqb i i').
-    case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto.
-    constructor. intros H; noconf H; auto.
-    constructor. intros H; noconf H; auto.
-    constructor. intros H; noconf H; auto.
-    change (eqb_prim_model f f') with (eqb f f').
-    case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
-    constructor. intros H; noconf H; auto.
-    constructor. intros H; noconf H; auto.
-    constructor. intros H; noconf H; auto.
-    change (eqb_prim_model a a') with (eqb a a').
-    case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
+    all: try by constructor; intros H; noconf H; auto.
+    - change (eqb_prim_model i i') with (eqb i i').
+      case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto.
+    - change (eqb_prim_model f f') with (eqb f f').
+      case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
+    - change (eqb_prim_model s s') with (eqb s s').
+      case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
+    - change (eqb_prim_model a a') with (eqb a a').
+      case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
   Qed.
 
   #[global]
-  Instance prim_tag_model_eqdec {req : ReflectEq term} : EqDec (prim_val) := _.
+    Instance prim_tag_model_eqdec {req : ReflectEq term} : EqDec (prim_val) := _.
 
   (** Printing *)
 
@@ -138,6 +155,7 @@ Section PrimModel.
     match p.π2 return string with
     | primIntModel f => "(int: " ^ string_of_prim_int f ^ ")"
     | primFloatModel f => "(float: " ^ string_of_float f ^ ")"
+    | primStringModel s => "(string: " ^ string_of_pstring s ^ ")"
     | primArrayModel a => "(array:" ^ soft a.(array_default) ^ " , " ^ string_of_list soft a.(array_value) ^ ")"
     end.
 
@@ -148,12 +166,14 @@ Section PrimModel.
     match p.π2 return bool with
     | primIntModel f => true
     | primFloatModel f => true
+    | primStringModel f => true
     | primArrayModel a => test_array_model f a
     end.
 
   Inductive primProp P : prim_val -> Type :=
     | primPropInt i : primProp P (primInt; primIntModel i)
     | primPropFloat f : primProp P (primFloat; primFloatModel f)
+    | primPropString s : primProp P (primString; primStringModel s)
     | primPropArray a : P a.(array_default) × All P a.(array_value) ->
         primProp P (primArray; primArrayModel a).
   Derive Signature NoConfusion for primProp.
@@ -162,6 +182,7 @@ Section PrimModel.
     match p.π2 return A with
     | primIntModel f => acc
     | primFloatModel f => acc
+    | primStringModel f => acc
     | primArrayModel a => fold_left f a.(array_value) (f acc a.(array_default))
     end.
 End PrimModel.
@@ -181,6 +202,7 @@ Section PrimOps.
     match p.π2 return prim_val term' with
     | primIntModel f => (primInt; primIntModel f)
     | primFloatModel f => (primFloat; primFloatModel f)
+    | primStringModel f => (primString; primStringModel f)
     | primArrayModel a => (primArray; primArrayModel (map_array_model f a))
     end.
 End PrimOps.
@@ -343,6 +365,7 @@ Section PrimIn.
   Equations InPrim (x : term) (p : prim_val term) : Prop :=
     | x | (primInt; primIntModel i) := False
     | x | (primFloat; primFloatModel _) := False
+    | x | (primString; primStringModel _) := False
     | x | (primArray; primArrayModel a) :=
       x = a.(array_default) \/ In x a.(array_value).
 
@@ -360,6 +383,7 @@ Section PrimIn.
   Equations test_primIn (p : prim_val term) (f : forall x : term, InPrim x p -> bool) : bool :=
     | (primInt; primIntModel i) | _ := true
     | (primFloat; primFloatModel _) | _ := true
+    | (primString; primStringModel _) | _ := true
     | (primArray; primArrayModel a) | f :=
       f a.(array_default) (or_introl eq_refl) && forallb_InP a.(array_value) (fun x H => f x (or_intror H)).
 
@@ -373,6 +397,7 @@ Section PrimIn.
   Equations map_primIn (p : prim_val term) (f : forall x : term, InPrim x p -> term) : prim_val term :=
     | (primInt; primIntModel i) | _ := (primInt; primIntModel i)
     | (primFloat; primFloatModel f) | _ := (primFloat; primFloatModel f)
+    | (primString; primStringModel f) | _ := (primString; primStringModel f)
     | (primArray; primArrayModel a) | f :=
       (primArray; primArrayModel
         {| array_default := f a.(array_default) (or_introl eq_refl);
@@ -455,6 +480,7 @@ Section onPrims.
   Inductive onPrims {term term' : Set} (R : term -> term' -> Set) : prim_val term -> prim_val term' -> Type :=
     | onPrimsInt i : onPrims R (primInt; primIntModel i) (primInt; primIntModel i)
     | onPrimsFloat f : onPrims R (primFloat; primFloatModel f) (primFloat; primFloatModel f)
+    | onPrimsString s : onPrims R (primString; primStringModel s) (primString; primStringModel s)
     | onPrimsArray v def v' def' :
       R def def' ->
       All2_Set R v v' ->
@@ -466,6 +492,7 @@ Section onPrims.
   Variant onPrims_dep {term term' : Set} (R : term -> term' -> Set) (P : forall x y, R x y -> Type) : forall x y, onPrims R x y -> Type :=
   | onPrimsIntDep i : onPrims_dep R P (prim_int i) (prim_int i) (onPrimsInt R i)
   | onPrimsFloatDep f : onPrims_dep R P (prim_float f) (prim_float f) (onPrimsFloat R f)
+  | onPrimsStringDep s : onPrims_dep R P (prim_string s) (prim_string s) (onPrimsString R s)
   | onPrimsArrayDep v def v' def'
     (ed : R def def')
     (ev : All2_Set R v v') :
@@ -485,6 +512,7 @@ Section onPrims.
     Equations map_onPrims {p : prim_val term} {p' : prim_val term'} (ev : onPrims R p p') : onPrims_dep R P p p' ev :=
     | @onPrimsInt _ _ _ _ := onPrimsIntDep _ _ i;
     | @onPrimsFloat _ _ _ _ := onPrimsFloatDep _ _ f;
+    | @onPrimsString _ _ _ _ := onPrimsStringDep _ _ s;
     | @onPrimsArray v def v' def' ed ev :=
       onPrimsArrayDep _ _ v def v' def' ed ev (F _ _ ed) (map_All2_dep _ F ev).
   End map_onPrims.
diff --git a/erasure/theories/EReflect.v b/erasure/theories/EReflect.v
index 70bb89dc6..b784392b6 100644
--- a/erasure/theories/EReflect.v
+++ b/erasure/theories/EReflect.v
@@ -115,6 +115,7 @@ Proof.
   - destruct prim as [? []]; destruct p as [? []]; cbn ; nodec.
     + destruct (eq_dec i i0); nodec; subst; eauto.
     + destruct (eq_dec f f0); nodec; subst; eauto.
+    + destruct (eq_dec s s0); nodec; subst; eauto.
     + destruct a as [? ?], a0 as [? ?]; cbn.
       depelim X. destruct p as [hd hv]. cbn in *.
       destruct (hd array_default); nodec; subst; eauto.
diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v
index 8a7344d94..2810058df 100644
--- a/erasure/theories/ERemoveParams.v
+++ b/erasure/theories/ERemoveParams.v
@@ -569,6 +569,7 @@ Module Fast.
         | None => mkApps (EAst.tConstruct kn c block_args) app }
     | app, tPrim (primInt; primIntModel i) => mkApps (tPrim (primInt; primIntModel i)) app
     | app, tPrim (primFloat; primFloatModel f) => mkApps (tPrim (primFloat; primFloatModel f)) app
+    | app, tPrim (primString; primStringModel f) => mkApps (tPrim (primString; primStringModel f)) app
     | app, tPrim (primArray; primArrayModel a) =>
       mkApps (tPrim (primArray; primArrayModel {| array_default := strip [] a.(array_default); array_value := strip_args a.(array_value) |})) app
     | app, tLazy t => mkApps (tLazy (strip [] t)) app
diff --git a/erasure/theories/EWcbvEval.v b/erasure/theories/EWcbvEval.v
index 3080d7fde..36058cee8 100644
--- a/erasure/theories/EWcbvEval.v
+++ b/erasure/theories/EWcbvEval.v
@@ -77,6 +77,7 @@ Section Wcbv.
   Variant eval_primitive {term term' : Set} (eval : term -> term' -> Set) : prim_val term -> prim_val term' -> Set :=
     | evalPrimInt i : eval_primitive eval (prim_int i) (prim_int i)
     | evalPrimFloat f : eval_primitive eval (prim_float f) (prim_float f)
+    | evalPrimString s : eval_primitive eval (prim_string s) (prim_string s)
     | evalPrimArray v def v' def'
       (ev : All2_Set eval v v')
       (ed : eval def def') :
@@ -88,6 +89,7 @@ Section Wcbv.
   Variant eval_primitive_ind {term term' : Set} (eval : term -> term' -> Set) (P : forall x y, eval x y -> Type) : forall x y, eval_primitive eval x y -> Type :=
   | evalPrimIntDep i : eval_primitive_ind eval P (prim_int i) (prim_int i) (evalPrimInt eval i)
   | evalPrimFloatDep f : eval_primitive_ind eval P (prim_float f) (prim_float f) (evalPrimFloat eval f)
+  | evalPrimStringDep s : eval_primitive_ind eval P (prim_string s) (prim_string s) (evalPrimString eval s)
   | evalPrimArrayDep v def v' def'
     (ev : All2_Set eval v v')
     (ed : eval def def') :
@@ -106,6 +108,7 @@ Section Wcbv.
     Equations map_eval_primitive {p : prim_val term} {p' : prim_val term'} (ev : eval_primitive eval p p') : eval_primitive_ind eval P p p' ev :=
     | @evalPrimInt _ _ _ _ := evalPrimIntDep _ _ i;
     | @evalPrimFloat _ _ _ _ := evalPrimFloatDep _ _ f;
+    | @evalPrimString _ _ _ _ := evalPrimStringDep _ _ s;
     | @evalPrimArray v def v' def'  ev ed :=
       evalPrimArrayDep _ _ v def v' def' ev ed (map_All2_dep _ F ev) (F _ _ ed).
   End map_eval_prim.
@@ -313,6 +316,7 @@ Section Wcbv.
    Variant primitive_value (value : term -> Type) : prim_val term -> Type :=
     | primIntValue i : primitive_value value (prim_int i)
     | primFloatValue f : primitive_value value (prim_float f)
+    | primStringValue s : primitive_value value (prim_string s)
     | primArrayValue a :
       All value a.(array_value) ->
       value a.(array_default) ->
@@ -343,8 +347,9 @@ Definition eval_primitive_depth {eval : term -> term -> Set} (size : forall x y,
   match e with
   | evalPrimInt _ => 0
   | evalPrimFloat _ => 0
+  | evalPrimString _ => 0
   | evalPrimArray v d v' d' aev ed =>
-    all2_size _ size aev + size _ _ ed
+      all2_size _ size aev + size _ _ ed
   end.
 
 Fixpoint eval_depth {wfl : WcbvFlags} {Σ : EAst.global_declarations} {t1 t2 : EAst.term} (ev : eval Σ t1 t2) { struct ev } : nat.
@@ -352,12 +357,12 @@ Proof.
   rename eval_depth into aux.
   destruct ev.
   all:try match goal with
-  | [ H : eval _ _ _, H' : eval _ _ _, H'' : eval _ _ _ |- _ ] =>
-    apply aux in H; apply aux in H'; apply aux in H''; exact (S (Nat.max H (Nat.max H' H'')))
-  | [ H : eval _ _ _, H' : eval _ _ _ |- _ ] =>
-    apply aux in H; apply aux in H'; exact (S (Nat.max H H'))
-  | [ H : eval _ _ _ |- _ ] => apply aux in H; exact (S H)
-  end.
+        | [ H : eval _ _ _, H' : eval _ _ _, H'' : eval _ _ _ |- _ ] =>
+            apply aux in H; apply aux in H'; apply aux in H''; exact (S (Nat.max H (Nat.max H' H'')))
+        | [ H : eval _ _ _, H' : eval _ _ _ |- _ ] =>
+            apply aux in H; apply aux in H'; exact (S (Nat.max H H'))
+        | [ H : eval _ _ _ |- _ ] => apply aux in H; exact (S H)
+        end.
   exact (S (all2_size _ (fun x y ev => aux wfl Σ x y ev) a)).
   exact (S (eval_primitive_depth (aux wfl Σ) e)).
   exact 1.
@@ -1833,7 +1838,7 @@ Proof.
     { induction a; cbn; try lia.
       destruct iha. destruct s. cbn. specialize (IHa a0). lia. }
   - unshelve eexists. eapply eval_app_cong; eauto. eapply IHHe1. eapply IHHe2. cbn. destruct IHHe1, IHHe2. lia.
-  - depelim X. 1-2:unshelve eexists; cbn; repeat constructor.
+  - depelim X. 1-3:unshelve eexists; cbn; repeat constructor.
     destruct s as [hev evd].
     unshelve eexists. do 2 econstructor.
     clear -a. induction ev; constructor. apply a. apply IHev, a. tea.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
index 5e4479327..891283ac8 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
@@ -551,6 +551,7 @@ Proof.
     1,3:(apply and_assum; [ih|hp' P'Q]).
     intros. apply and_assum; [ih|hp' P'Q].
   - unshelve eapply Qprim; tea. depelim e.
+    * constructor.
     * constructor.
     * constructor.
     * eapply Qpres in qt. depelim qt. now cbn in i. constructor; eauto.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
index 111033e35..c4b52691a 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
@@ -451,6 +451,7 @@ Proof.
     1,3:(apply and_assum; [ih|hp' P'Q]).
     intros. apply and_assum; [ih|hp' P'Q].
   - unshelve eapply Qprim; tea. depelim e.
+    * constructor.
     * constructor.
     * constructor.
     * eapply Qpres in qt. depelim qt. now cbn in i. constructor; eauto.
diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v
index 126667ae3..d048beb4d 100644
--- a/erasure/theories/EWcbvEvalEtaInd.v
+++ b/erasure/theories/EWcbvEvalEtaInd.v
@@ -692,6 +692,7 @@ Proof.
     depelim e.
     * split; simp_eta. unshelve eapply Qprim. constructor. constructor.
     * split; simp_eta. unshelve eapply Qprim. constructor. constructor.
+    * split; simp_eta. unshelve eapply Qprim. constructor. constructor.
     * eapply Qpres in qt. depelim qt. now cbn in i.
       split; simp_eta. unshelve eapply Qprim. constructor; eauto. constructor.
       + apply All2_over_undep. cbn in IH.
diff --git a/erasure/theories/EWellformed.v b/erasure/theories/EWellformed.v
index 78e3a6422..0ad7268a3 100644
--- a/erasure/theories/EWellformed.v
+++ b/erasure/theories/EWellformed.v
@@ -23,12 +23,14 @@ Definition isSome {A} (o : option A) :=
 Class EPrimitiveFlags :=
   { has_primint : bool;
     has_primfloat : bool;
+    has_primstring : bool;
     has_primarray : bool }.
 
 Definition has_prim {epfl : EPrimitiveFlags} (p : prim_val term) :=
   match p.π1 with
   | primInt => has_primint
   | primFloat => has_primfloat
+  | primString => has_primstring
   | primArray => has_primarray
   end.
 
@@ -60,6 +62,7 @@ Class EEnvFlags := {
 Definition all_primitive_flags :=
   {| has_primint := true;
      has_primfloat := true;
+     has_primstring := true;
      has_primarray := true |}.
 
 Lemma has_prim_all_primitive_flags p : @has_prim all_primitive_flags p.
diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
index 6cd516743..db6bc66a7 100644
--- a/erasure/theories/ErasureCorrectness.v
+++ b/erasure/theories/ErasureCorrectness.v
@@ -1165,6 +1165,8 @@ Proof.
       depelim X. constructor.
     + exists (EAst.tPrim (EPrimitive.prim_float f)); split => //; repeat constructor.
       depelim X. constructor.
+    + exists (EAst.tPrim (EPrimitive.prim_string s)); split => //; repeat constructor.
+      depelim X. constructor.
     + depelim X. subst a0 a'; cbn in *.
       depelim Hed; cbn in *.
       eapply inversion_Prim in Hty as [prim_ty [cdecl []]]; cbn in *; eauto.
@@ -1409,7 +1411,7 @@ Proof.
           solve_all.
   - intros Γ0 v etaΣ er.
     depelim er; eauto. depelim H1.
-    depelim H0. 1-2:depelim X; repeat constructor.
+    depelim H0. 1-3:depelim X; repeat constructor.
     depelim X0. eapply expanded_tPrim. constructor; split => //; cbn.
     eapply H0; tea. now depelim etaΣ; cbn in *.
     eapply Forall_All. depelim etaΣ. cbn in *.
diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v
index 75efbea4f..89edfe784 100644
--- a/erasure/theories/ErasureFunction.v
+++ b/erasure/theories/ErasureFunction.v
@@ -1026,6 +1026,7 @@ Section Erase.
         E.tCoFix mfix' n
       | tPrim (primInt; PCUICPrimitive.primIntModel i) := E.tPrim (primInt; EPrimitive.primIntModel i) ;
       | tPrim (primFloat; PCUICPrimitive.primFloatModel f) := E.tPrim (primFloat; EPrimitive.primFloatModel f) ;
+      | tPrim (primString; PCUICPrimitive.primStringModel s) := E.tPrim (primString; EPrimitive.primStringModel s) ;
       | tPrim (primArray; PCUICPrimitive.primArrayModel a) :=
         E.tPrim (primArray; EPrimitive.primArrayModel
           {| EPrimitive.array_default := erase Γ a.(PCUICPrimitive.array_default) _;
@@ -1276,6 +1277,7 @@ Proof.
     intros isp. eapply isErasable_Proof in isp.
     eapply H'; intros. now rewrite (abstract_env_ext_irr _ H0 H).
 
+  - repeat constructor.
   - repeat constructor.
   - repeat constructor.
   - repeat constructor; eauto.
diff --git a/erasure/theories/Extract.v b/erasure/theories/Extract.v
index 3a3f72ee9..c5ca0ec26 100644
--- a/erasure/theories/Extract.v
+++ b/erasure/theories/Extract.v
@@ -71,6 +71,7 @@ Inductive erase_prim_model (erase : term -> E.term -> Prop) : forall {t : prim_t
   @PCUICPrimitive.prim_model term t -> @prim_model E.term t -> Type :=
 | erase_primInt i : @erase_prim_model erase primInt (PCUICPrimitive.primIntModel i) (primIntModel i)
 | erase_primFloat f : @erase_prim_model erase primFloat (PCUICPrimitive.primFloatModel f) (primFloatModel f)
+| erase_primString s : @erase_prim_model erase primString (PCUICPrimitive.primStringModel s) (primStringModel s)
 | erase_primArray a ed ev :
     erase a.(PCUICPrimitive.array_default) ed ->
     All2 erase a.(PCUICPrimitive.array_value) ev ->
@@ -357,6 +358,8 @@ Inductive erases_deps (Σ : global_env) (Σ' : E.global_declarations) : E.term -
     erases_deps Σ Σ' (E.tPrim (primInt; primIntModel i))
 | erases_deps_tPrimFloat f :
     erases_deps Σ Σ' (E.tPrim (primFloat; primFloatModel f))
+| erases_deps_tPrimString s :
+    erases_deps Σ Σ' (E.tPrim (primString; primStringModel s))
 | erases_deps_tPrimArray a :
     erases_deps Σ Σ' a.(array_default) ->
     Forall (erases_deps Σ Σ') a.(array_value) ->
diff --git a/erasure/theories/Typed/Certifying.v b/erasure/theories/Typed/Certifying.v
index e2c693743..64920a579 100644
--- a/erasure/theories/Typed/Certifying.v
+++ b/erasure/theories/Typed/Certifying.v
@@ -51,6 +51,7 @@ Definition change_modpath (mpath : modpath) (suffix : string) (to_rename : kerna
     | tCoFix mfix idx => tCoFix (map (map_def go go) mfix) idx
     | tInt n => tInt n
     | tFloat n => tFloat n
+    | tString n => tString n
     | tArray l v def ty => tArray l (map go v) (go def) (go ty)
   end.
 
diff --git a/erasure/theories/Typed/WcbvEvalAux.v b/erasure/theories/Typed/WcbvEvalAux.v
index 7f3a7d649..616729500 100644
--- a/erasure/theories/Typed/WcbvEvalAux.v
+++ b/erasure/theories/Typed/WcbvEvalAux.v
@@ -279,7 +279,7 @@ Qed.
 
 Definition eval_prim_length {wfl : WcbvFlags} {Σ p p'} (len : forall t v, Σ e⊢ t ⇓ v -> nat) (d : eval_primitive (eval Σ) p p') : nat :=
   match d with
-  | evalPrimInt _ | evalPrimFloat _ => 0
+  | evalPrimInt _ | evalPrimFloat _ | evalPrimString _ => 0
   | evalPrimArray v d v' d' av ev =>
     len _ _ ev + EPrimitive.all2_size _ len av
   end.
diff --git a/pcuic/theories/Bidirectional/BDFromPCUIC.v b/pcuic/theories/Bidirectional/BDFromPCUIC.v
index d92a5a6fb..e8f2d5220 100644
--- a/pcuic/theories/Bidirectional/BDFromPCUIC.v
+++ b/pcuic/theories/Bidirectional/BDFromPCUIC.v
@@ -362,7 +362,7 @@ Proof.
 
   - intros p prim_ty cdecl wfΓ' hp hdecl pinv.
     eexists. split; [econstructor; tea|].
-    destruct X0. 1-2:constructor; eauto.
+    destruct X0. 1-3:constructor; eauto.
     eapply conv_check in hty; tea.
     eapply conv_check in hdef; tea.
     constructor; eauto. solve_all.
diff --git a/pcuic/theories/Bidirectional/BDUnique.v b/pcuic/theories/Bidirectional/BDUnique.v
index 13bb91a57..baba70a9f 100644
--- a/pcuic/theories/Bidirectional/BDUnique.v
+++ b/pcuic/theories/Bidirectional/BDUnique.v
@@ -241,6 +241,7 @@ Proof using wfΣ.
   - depelim X; depelim X0.
     * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs.
     * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs.
+    * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs.
     * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs.
       all:simp prim_type; cbn. cbn in hty.
       all:eapply type_is_open_term, checking_typing; tea.
diff --git a/pcuic/theories/PCUICAlpha.v b/pcuic/theories/PCUICAlpha.v
index 763e5da3f..b0d746fbe 100644
--- a/pcuic/theories/PCUICAlpha.v
+++ b/pcuic/theories/PCUICAlpha.v
@@ -880,7 +880,7 @@ Section Alpha.
       + apply eq_term_upto_univ_cumulSpec, eq_term_leq_term, upto_names_impl_eq_term.
         now symmetry.
     - intros p prim_ty cdecl IH prim decl pinv pty ptyIH Δ v e e'.
-      depelim e. depelim o. 1-2:econstructor; eauto; constructor.
+      depelim e. depelim o. 1-3:econstructor; eauto; constructor.
       pose proof (validity (type_Prim Σ Γ _ _ _ wfΓ prim decl pinv pty)) as (_ & s & Hs & _).
       eapply type_Cumul. econstructor; eauto.
       * depelim ptyIH. constructor; eauto. now rewrite -e. rewrite -e; eauto.
diff --git a/pcuic/theories/PCUICAst.v b/pcuic/theories/PCUICAst.v
index c6f0f19c6..7c802bfcd 100644
--- a/pcuic/theories/PCUICAst.v
+++ b/pcuic/theories/PCUICAst.v
@@ -216,6 +216,7 @@ Notation prim_val := (prim_val term).
 
 Notation tInt i := (tPrim (_; primIntModel i)) (only parsing).
 Notation tFloat f := (tPrim (_; primFloatModel f)) (only parsing).
+Notation tString s := (tPrim (_; primStringModel s)) (only parsing).
 
 Fixpoint mkApps t us :=
   match us with
diff --git a/pcuic/theories/PCUICClassification.v b/pcuic/theories/PCUICClassification.v
index b67bb8e05..c76e23e21 100644
--- a/pcuic/theories/PCUICClassification.v
+++ b/pcuic/theories/PCUICClassification.v
@@ -813,7 +813,7 @@ Section classification.
     - now rewrite head_mkApps /head /=.
     - eapply inversion_Prim in typed as [prim_ty [cdecl [? ? ? ? hp]]]; eauto.
       destruct p as [? []]; simp prim_type in w.
-      1-2:eapply (invert_cumul_axiom_ind (args := [])) in w; eauto; destruct p0 as [s []]; eauto.
+      1-3:eapply (invert_cumul_axiom_ind (args := [])) in w; eauto; destruct p0 as [? []]; eauto.
       eapply (invert_cumul_axiom_ind (args := [array_type a0])) in w; eauto. destruct p0 as [s []]; eauto.
   Qed.
 
@@ -1082,7 +1082,7 @@ Section classification.
       now eapply red_app.
 
     - eapply inversion_Prim in Ht as [prim_type [decl []]]; eauto.
-      depelim X. 1-2:reflexivity.
+      depelim X. 1-3:reflexivity.
       depelim p1. specialize (r _ hdef).
       eapply red_primArray_congr; eauto.
       eapply All2_undep in a. solve_all.
diff --git a/pcuic/theories/PCUICConversion.v b/pcuic/theories/PCUICConversion.v
index 0f23a2563..84bb27af6 100644
--- a/pcuic/theories/PCUICConversion.v
+++ b/pcuic/theories/PCUICConversion.v
@@ -847,6 +847,7 @@ Section ConvCongruences.
     Σ ;;; Γ ⊢ tPrim p ⇝ T ->
     (∑ i, p = (primInt; primIntModel i) /\ T = tPrim p) +
     (∑ f, p = (primFloat; primFloatModel f) /\ T = tPrim p) +
+    (∑ s, p = (primString; primStringModel s) /\ T = tPrim p) +
     ∑ a a',
       [× p = (primArray; primArrayModel a), T = tPrim (primArray; primArrayModel a'),
         a.(array_level) = a'.(array_level),
@@ -859,6 +860,7 @@ Section ConvCongruences.
     apply: closed_red_ind; intros; subst.
     - destruct p as [? []].
       * now left.
+      * left. left. now right.
       * left. now right.
       * right. exists a, a.
         cbn in H0; rtoProp; intuition auto.
@@ -882,14 +884,17 @@ Section ConvCongruences.
         * eapply into_closed_red; eauto.
         * toAll; eapply All_All2; tea; cbn; intuition eauto using into_closed_red.
     - specialize (X1 _ eq_refl) as [].
-      * destruct s as [[? []]|[? []]]; subst;
+      * destruct s as [[[? []]|[? []]]|[? []]]; subst;
         specialize (X2 _ eq_refl) as [].
         + left. destruct s; [left|right]; eauto.
         + destruct s as [? [? []]]. subst. noconf e.
         + left; destruct s; [left|right]; eauto.
         + destruct s as [? [? []]]; subst; noconf e.
+        + left; destruct s; [left|right]; eauto.
+        + destruct s as [? [? []]]; subst; noconf e.
       * right. destruct s as [a [a' []]].
-        subst. specialize (X2 _ eq_refl) as [[|]|].
+        subst. specialize (X2 _ eq_refl) as [[[|]|]|].
+        + destruct s as [? []]; congruence.
         + destruct s as [? []]; congruence.
         + destruct s as [? []]; congruence.
         + destruct s as [a2 [a2' []]]; subst.
@@ -1461,7 +1466,7 @@ Section Inversions.
   Proof using wfΣ.
     intros hd hb ht.
     destruct p as [? []]; simp prim_type in ht.
-    1-2:eapply (invert_cumul_axiom_ind (args := [])) in ht; tea; now destruct hb as [s []].
+    1-3:eapply (invert_cumul_axiom_ind (args := [])) in ht; tea; now destruct hb as [? []].
     eapply (invert_cumul_axiom_ind (args := [_])) in ht; tea. apply hb.
   Qed.
 
@@ -1472,7 +1477,7 @@ Section Inversions.
   Proof using wfΣ.
     intros hd hb ht.
     destruct p as [? []]; simp prim_type in ht.
-    1-2:eapply (invert_cumul_axiom_prod (args := [])) in ht; tea; now destruct hb as [s []].
+    1-3:eapply (invert_cumul_axiom_prod (args := [])) in ht; tea; now destruct hb as [? []].
     eapply (invert_cumul_axiom_prod (args := [_])) in ht; tea. apply hb.
   Qed.
 
@@ -1485,8 +1490,9 @@ Section Inversions.
     move/ws_cumul_pb_alt_closed: hd => [v [v' []]].
     move/invert_red_tPrim => hl.
     move/invert_red_tPrim => hr.
-    destruct hl as [[[i []]|[f []]]|[a [a' []]]],
-       hr as [[[i' []]|[f' []]]|[a1 [a2' []]]]; subst; try congruence;
+
+    destruct hl as [[[[i []]|[f []]]|[s []]]|[a [a' []]]],
+      hr as [[[[i' []]|[f' []]]|[s' []]]|[a1 [a2' []]]]; subst; try congruence;
      intros eq; depelim eq; depelim o; cbn in cl', cl'';
       rtoProp; intuition eauto; constructor; eauto.
     - rewrite e1 e4 //.
@@ -3903,7 +3909,7 @@ Lemma ws_cumul_pb_Prim {pb Γ p p'} :
   Σ;;; Γ ⊢ tPrim p ≤[pb] tPrim p'.
 Proof.
   intros Hp HΓ.
-  depelim Hp. 1-2:constructor; eauto; trea.
+  depelim Hp. 1-3:constructor; eauto; trea.
   apply ws_cumul_pb_terms_alt in a0 as [args0 [args0'  [Hargs0 Hargs0' Hargs0args0']]].
   pose proof (Hargs0_c :=  closed_red_terms_open_right Hargs0).
   pose proof (Hargs0'_c :=  closed_red_terms_open_right Hargs0').
diff --git a/pcuic/theories/PCUICCumulProp.v b/pcuic/theories/PCUICCumulProp.v
index 3f5ce1201..129f87810 100644
--- a/pcuic/theories/PCUICCumulProp.v
+++ b/pcuic/theories/PCUICCumulProp.v
@@ -819,7 +819,7 @@ Qed.
 Lemma untyped_subslet_inds Γ ind u u' mdecl :
   untyped_subslet Γ (inds (inductive_mind ind) u (ind_bodies mdecl))
     (subst_instance u' (arities_context (ind_bodies mdecl))).
-Proof using Type.
+Proof using Type Hcf cf.
   generalize (le_n #|ind_bodies mdecl|).
   generalize (ind_bodies mdecl) at 1 3 4.
   unfold inds.
@@ -894,7 +894,7 @@ Lemma cumul_prop_mkApps {Σ Γ f args f' args'} {wfΣ : wf_ext Σ} :
   eq_term Σ.1 Σ f f' ->
   All2 (cumul_prop Σ Γ) args args' ->
   Σ ;;; Γ |- mkApps f args ~~ mkApps f' args'.
-Proof using Type.
+Proof using Type Hcf cf.
   intros clΓ clf clf' eq eq'.
   eapply cumul_prop_alt.
   eapply cumul_prop_args in eq' as (nf & nf' & [redl redr eq']).
@@ -997,7 +997,7 @@ Lemma typing_leq_term_prop_gen :
       forall pb n, compare_term_napp Σ Σ pb n t' t ->
       Σ ;;; Γ |- T ~~ T') j)
     (fun Σ Γ => wf_local Σ Γ).
-Proof using Type.
+Proof using Type Hcf cf.
   eapply typing_ind_env.
   { intros ???? H ?. apply lift_typing_impl with (1 := H) => ?? [] ?? ?? //. eauto. }
   1: now auto.
@@ -1227,7 +1227,7 @@ Proof using Type.
 
   - depelim X3.
     eapply inversion_Prim in X2 as [prim_ty' [cdecl' []]]; tea. depelim o.
-    1-2:rewrite H in e; noconf e; eapply cumul_pb_cumul_prop; eauto; pcuic.
+    1-3:rewrite H in e; noconf e; eapply cumul_pb_cumul_prop; eauto; pcuic.
     depelim X1.
     cbn in H, e2. rewrite H in e2. noconf e2. eapply cumul_pb_cumul_prop; eauto; pcuic.
     move: w; simp prim_type. intro. etransitivity; tea. constructor; fvs. cbn.
@@ -1241,7 +1241,7 @@ Lemma typing_leq_term_prop (Σ : global_env_ext) Γ t t' T T' :
   Σ ;;; Γ |- t' : T' ->
   forall pb n, compare_term_napp Σ Σ pb n t' t ->
   Σ ;;; Γ |- T ~~ T'.
-Proof using Type.
+Proof using Type Hcf cf.
   intros.
   now eapply (env_prop_typing typing_leq_term_prop_gen).
 Qed.
@@ -1251,7 +1251,7 @@ Lemma typing_cumul_term_prop {Σ : global_env_ext} {wfΣ : wf_ext Σ} pb Γ t t'
   Σ ;;; Γ |- t' : T' ->
   Σ ;;; Γ |- t' <=[pb] t ->
   Σ ;;; Γ |- T ~~ T'.
-Proof using Type.
+Proof using Type Hcf cf.
   intros.
   apply cumul_alt in X1 as (v & v' & r & r' & leq).
   eapply typing_leq_term_prop. 5: eassumption. 1,3: apply wfΣ.
diff --git a/pcuic/theories/PCUICEtaExpand.v b/pcuic/theories/PCUICEtaExpand.v
index 03e6336be..4da68699b 100644
--- a/pcuic/theories/PCUICEtaExpand.v
+++ b/pcuic/theories/PCUICEtaExpand.v
@@ -58,6 +58,7 @@ Section map_onPrim.
     match o with
     | onPrimInt i => onPrimInt _ i
     | onPrimFloat f => onPrimFloat _ f
+    | onPrimString s => onPrimString _ s
     | onPrimArray a def ty v =>
       onPrimArray _ _ (ont _ def) (ont _ ty) (map_All _ _ ont v)
     end.
diff --git a/pcuic/theories/PCUICNormal.v b/pcuic/theories/PCUICNormal.v
index b84636432..afeafcc68 100644
--- a/pcuic/theories/PCUICNormal.v
+++ b/pcuic/theories/PCUICNormal.v
@@ -1048,7 +1048,7 @@ Proof.
     cbn.
     intros ? ? (->&->&r1&r2).
     eauto.
-  - depelim o. 1-2: reflexivity.
+  - depelim o. 1-3: reflexivity.
     eapply red_primArray_congr; eauto.
     now eapply Universe.make'_inj in e.
 Qed.
diff --git a/pcuic/theories/PCUICParallelReductionConfluence.v b/pcuic/theories/PCUICParallelReductionConfluence.v
index 886f13f3c..8b7611754 100644
--- a/pcuic/theories/PCUICParallelReductionConfluence.v
+++ b/pcuic/theories/PCUICParallelReductionConfluence.v
@@ -501,6 +501,7 @@ Section Rho.
   Equations? map_prim_wf (p : PCUICPrimitive.prim_val term) (rho : context -> forall x, depth x < depth (tPrim p) -> term) (Γ : context) : prim_val :=
   | (primInt; primIntModel i), _, _ := (primInt; primIntModel i);
   | (primFloat; primFloatModel f), _, _ := (primFloat; primFloatModel f);
+  | (primString; primStringModel s), _, _ := (primString; primStringModel s);
   | (primArray; primArrayModel a), rho, Γ :=
     let default := rho Γ a.(array_default) _ in
     let ty := rho Γ a.(array_type) _ in
diff --git a/pcuic/theories/PCUICPrincipality.v b/pcuic/theories/PCUICPrincipality.v
index 81654c126..7838e1513 100644
--- a/pcuic/theories/PCUICPrincipality.v
+++ b/pcuic/theories/PCUICPrincipality.v
@@ -716,7 +716,7 @@ Proof.
 
   - epose proof (type_Prim _ _ _ _ _ X H H0 H1 X0). eapply validity in X4.
     depelim X1; depelim X3; depelim o.
-    1-2:econstructor; tea.
+    1-3:econstructor; tea.
     depelim X0. destruct X4 as (_ & s & ? & _).
     econstructor; tea.
     eapply inversion_Prim in X2 as [prim_ty' [cdecl' []]]; eauto.
diff --git a/pcuic/theories/PCUICProgress.v b/pcuic/theories/PCUICProgress.v
index cefec7006..522e886eb 100644
--- a/pcuic/theories/PCUICProgress.v
+++ b/pcuic/theories/PCUICProgress.v
@@ -587,7 +587,7 @@ Proof.
   intros hdecl hb.
   induction args => //.
   destruct prim as [? []]; cbn in *; intros sp; destruct hb; simp prim_type in *.
-  1-2:eapply (typing_spine_axiom _ _ _ _ []) in sp; tea.
+  1-3:eapply (typing_spine_axiom _ _ _ _ []) in sp; tea.
   eapply (typing_spine_axiom _ _ _ _ [array_type a0]) in sp; tea.
 Qed.
 
@@ -782,6 +782,7 @@ Proof with eauto with wcbv; try congruence.
       eapply value_mkApps_inv in Hval as [[-> ]|[]]; eauto.
   - intros Σ wfΣ Γ _ p c u mdecl idecl cdecl pdecl Hcon args Hargs -> hp.
     depelim args... 1-2:right; constructor; constructor 2; constructor.
+    right. constructor. constructor 2. constructor.
     depelim Hcon.
     destruct hdef; eauto.
     + left. destruct s as [t' hred]. exists (tPrim (prim_array (set_array_default a t'))). now constructor.
diff --git a/pcuic/theories/PCUICTyping.v b/pcuic/theories/PCUICTyping.v
index 6d66e1f6a..8ea666590 100644
--- a/pcuic/theories/PCUICTyping.v
+++ b/pcuic/theories/PCUICTyping.v
@@ -178,6 +178,7 @@ Variant primitive_typing_hyps `{checker_flags}
   Σ Γ : prim_val term -> Type :=
 | prim_int_hyps i : primitive_typing_hyps typing Σ Γ (primInt; primIntModel i)
 | prim_float_hyps f : primitive_typing_hyps typing Σ Γ (primFloat; primFloatModel f)
+| prim_string_hyps s : primitive_typing_hyps typing Σ Γ (primString; primStringModel s)
 | prim_array_hyps a
   (wfl : wf_universe Σ (Universe.make' a.(array_level)))
   (hty : typing Σ Γ a.(array_type) (tSort (sType (Universe.make' a.(array_level)))))
@@ -189,6 +190,7 @@ Derive Signature for primitive_typing_hyps.
 Equations prim_type (p : prim_val term) (cst : kername) : term :=
 prim_type (primInt; _) cst := tConst cst [];
 prim_type (primFloat; _) cst := tConst cst [];
+prim_type (primString; _) cst := tConst cst [];
 prim_type (primArray; primArrayModel a) cst := tApp (tConst cst [a.(array_level)]) a.(array_type).
 Transparent prim_type.
 
@@ -409,6 +411,7 @@ Section PrimitiveSize.
     destruct h.
     - exact 0.
     - exact 0.
+    - exact 0.
     - exact (Nat.max (typing_size _ _ _ _ hty) (Nat.max (typing_size _ _ _ _ hdef)
         (all_size _ (fun x p => typing_size _ _ _ _ p) hvalue))).
   Defined.
diff --git a/pcuic/theories/PCUICValidity.v b/pcuic/theories/PCUICValidity.v
index ca255c23c..817c746b1 100644
--- a/pcuic/theories/PCUICValidity.v
+++ b/pcuic/theories/PCUICValidity.v
@@ -340,7 +340,7 @@ Section Validity.
 
     - (* Primitive *)
       depelim X0; depelim X1; simp prim_type; cbn in *.
-      1-2:destruct H1 as [hty hbod huniv]; eapply has_sort_isType with (s := _@[[]]); change (tSort ?s@[[]]) with (tSort s)@[[]];
+      1-3:destruct H1 as [hty hbod huniv]; eapply has_sort_isType with (s := _@[[]]); change (tSort ?s@[[]]) with (tSort s)@[[]];
           rewrite <- hty; refine (type_Const _ _ _ [] _ wfΓ H0 _); rewrite huniv //.
       set (s := sType (Universe.make' (array_level a))).
       destruct H1 as [hty' hbod huniv].
diff --git a/pcuic/theories/PCUICWcbvEval.v b/pcuic/theories/PCUICWcbvEval.v
index 56d56895d..d04ba3361 100644
--- a/pcuic/theories/PCUICWcbvEval.v
+++ b/pcuic/theories/PCUICWcbvEval.v
@@ -205,6 +205,7 @@ Section Wcbv.
   Variant eval_primitive (eval : term -> term -> Type) : prim_val -> prim_val -> Type :=
     | evalPrimInt i : eval_primitive eval (prim_int i) (prim_int i)
     | evalPrimFloat f : eval_primitive eval (prim_float f) (prim_float f)
+    | evalPrimString s : eval_primitive eval (prim_string s) (prim_string s)
     | evalPrimArray  u v def ty v' def'
       (ev : All2 eval v v')
       (ed : eval def def') :
@@ -216,6 +217,7 @@ Section Wcbv.
   Variant eval_primitive_ind (eval : term -> term -> Type) (P : forall x y, eval x y -> Type) : forall x y, eval_primitive eval x y -> Type :=
   | evalPrimIntDep i : eval_primitive_ind eval P (prim_int i) (prim_int i) (evalPrimInt eval i)
   | evalPrimFloatDep f : eval_primitive_ind eval P (prim_float f) (prim_float f) (evalPrimFloat eval f)
+  | evalPrimStringDep s : eval_primitive_ind eval P (prim_string s) (prim_string s) (evalPrimString eval s)
   | evalPrimArrayDep u v def ty v' def'
     (ev : All2 eval v v')
     (ed : eval def def') :
@@ -482,6 +484,7 @@ Section Wcbv.
    Variant primitive_value (value : term -> Type) : prim_val -> Type :=
     | primIntValue i : primitive_value value (prim_int i)
     | primFloatValue f : primitive_value value (prim_float f)
+    | primStringValue s : primitive_value value (prim_string s)
     | primArrayValue a :
       All value a.(array_value) ->
       value a.(array_default) ->
diff --git a/pcuic/theories/Syntax/PCUICPosition.v b/pcuic/theories/Syntax/PCUICPosition.v
index 39638242b..476804ef7 100644
--- a/pcuic/theories/Syntax/PCUICPosition.v
+++ b/pcuic/theories/Syntax/PCUICPosition.v
@@ -857,11 +857,11 @@ Proof.
     + simpl. destruct nth_error as [[na ty bo ra]|] eqn:e.
       * apply IHp.
       * rewrite hh. reflexivity.
-    + destruct prim as [? []]; simpl. 1-2:now rewrite hh.
+    + destruct prim as [? []]; simpl. 1-3:now rewrite hh.
       now rewrite IHp.
-    + destruct prim as [? []]; simpl. 1-2:now rewrite hh.
+    + destruct prim as [? []]; simpl. 1-3:now rewrite hh.
       now rewrite IHp.
-    + destruct prim as [? []]; simpl. 1-2:now rewrite hh.
+    + destruct prim as [? []]; simpl. 1-3:now rewrite hh.
       destruct nth_error eqn:e.
       * now rewrite IHp.
       * now rewrite hh.
diff --git a/pcuic/theories/Syntax/PCUICReflect.v b/pcuic/theories/Syntax/PCUICReflect.v
index 15a6b788e..d9b2c0cb2 100644
--- a/pcuic/theories/Syntax/PCUICReflect.v
+++ b/pcuic/theories/Syntax/PCUICReflect.v
@@ -246,6 +246,7 @@ Proof.
       destruct (eqb_spec rarg rarg0); t'.
       destruct (eqb_spec dname dname0); t'. }
   - destruct p, p; cbn in *; destruct prim, p; cbn; nodec.
+    case: eqb_spec; intros; subst; nodec. constructor; auto.
     case: eqb_spec; intros; subst; nodec. constructor; auto.
     case: eqb_spec; intros; subst; nodec. constructor; auto.
     destruct X as [eqty [eqd eqv]]. unfold eqb_array.
diff --git a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v
index f4cb79137..721fe0a39 100644
--- a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v
+++ b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v
@@ -86,11 +86,12 @@ Lemma extends_primitive_constant Σ Σ' p t :
 Proof.
   intros [_ _ ext].
   unfold primitive_constant.
-  case: ext => o [] o' o''.
+  case: ext => o [] o' [] o'' o'''.
   destruct p => //.
   - intros hr. now rewrite hr in o; depelim o.
   - intros hr. now rewrite hr in o'; depelim o'.
   - intros hr. now rewrite hr in o''; depelim o''.
+  - intros hr. now rewrite hr in o'''; depelim o'''.
 Qed.
 Local Hint Resolve extends_primitive_constant : extends.
 
diff --git a/pcuic/theories/utils/PCUICPretty.v b/pcuic/theories/utils/PCUICPretty.v
index 94065d591..72444c3cf 100644
--- a/pcuic/theories/utils/PCUICPretty.v
+++ b/pcuic/theories/utils/PCUICPretty.v
@@ -121,6 +121,7 @@ Module PrintTermTree.
       match p.π2 return Tree.t with
       | primIntModel f => "(int: " ^ show f ^ ")"
       | primFloatModel f => "(float: " ^ show f ^ ")"
+      | primStringModel s => "(string: " ^ show s ^ ")"
       | primArrayModel a => "(array:" ^ string_of_list soft a.(array_value) ^ ")"
       end.
 
diff --git a/pcuic/theories/utils/PCUICPrimitive.v b/pcuic/theories/utils/PCUICPrimitive.v
index 9807da587..ea6b9dc42 100644
--- a/pcuic/theories/utils/PCUICPrimitive.v
+++ b/pcuic/theories/utils/PCUICPrimitive.v
@@ -25,10 +25,12 @@ Proof. eqdec_proof. Qed.
 Inductive prim_model (term : Type) : prim_tag -> Type :=
 | primIntModel (i : PrimInt63.int) : prim_model term primInt
 | primFloatModel (f : PrimFloat.float) : prim_model term primFloat
+| primStringModel (s : PrimString.string) : prim_model term primString
 | primArrayModel (a : array_model term) : prim_model term primArray.
 
 Arguments primIntModel {term}.
 Arguments primFloatModel {term}.
+Arguments primStringModel {term}.
 Arguments primArrayModel {term}.
 
 Derive Signature NoConfusion NoConfusionHom for prim_model.
@@ -37,6 +39,7 @@ Definition prim_model_of (term : Type) (p : prim_tag) : Type :=
   match p with
   | primInt => PrimInt63.int
   | primFloat => PrimFloat.float
+  | primString => PrimString.string
   | primArray => array_model term
   end.
 
@@ -46,12 +49,14 @@ Definition prim_val_model {term} (s : prim_val term) : prim_model term (prim_val
 
 Definition prim_int {term} i : prim_val term := (primInt; primIntModel i).
 Definition prim_float {term} f : prim_val term := (primFloat; primFloatModel f).
+Definition prim_string {term} s : prim_val term := (primString; primStringModel s).
 Definition prim_array {term} a : prim_val term := (primArray; primArrayModel a).
 
 Definition prim_model_val {term} (p : prim_val term) : prim_model_of term (prim_val_tag p) :=
   match prim_val_model p in prim_model _ t return prim_model_of term t with
   | primIntModel i => i
   | primFloatModel f => f
+  | primStringModel s => s
   | primArrayModel a => a
   end.
 
@@ -101,9 +106,23 @@ Next Obligation.
   all:constructor; congruence.
 Qed.
 
+#[program,global]
+Instance reflect_eq_pstring : ReflectEq PrimString.string :=
+  { eqb := (fun s1 s2 => match PrimString.compare s1 s2 with Eq => true | _ => false end) }.
+Next Obligation. discriminate. Qed.
+Next Obligation. discriminate. Qed.
+Next Obligation.
+  intros s1 s2. simpl.
+  destruct (PrimString.compare s1 s2) eqn:Hcmp; constructor.
+  - by apply PString.string_eq_spec in Hcmp.
+  - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp.
+  - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp.
+Qed.
+
 Equations eqb_prim_model {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} {t : prim_tag} (x y : prim_model term t) : bool :=
   | primIntModel x, primIntModel y := ReflectEq.eqb x y
   | primFloatModel x, primFloatModel y := ReflectEq.eqb x y
+  | primStringModel x, primStringModel y := ReflectEq.eqb x y
   | primArrayModel x, primArrayModel y := eqb_array (equ := equ) (eqt:=req) x y.
 
 #[global, program]
@@ -113,6 +132,7 @@ Next Obligation.
   intros. depelim x; depelim y; simp eqb_prim_model.
   case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
   case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
+  case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
   change (eqb_array a a0) with (eqb a a0).
   case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
 Qed.
@@ -123,6 +143,7 @@ Instance prim_model_eqdec {term} {req : ReflectEq term} : forall p : prim_tag, E
 Equations eqb_prim_val {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} (x y : prim_val term) : bool :=
   | (primInt; i), (primInt; i') := eqb_prim_model (equ := equ) (req := req) i i'
   | (primFloat; f), (primFloat; f') := eqb_prim_model (equ := equ) (req := req) f f'
+  | (primString; s), (primString; s') := eqb_prim_model (equ := equ) (req := req) s s'
   | (primArray; a), (primArray; a') := eqb_prim_model (equ := equ) (req := req) a a'
   | x, y := false.
 
@@ -131,22 +152,19 @@ Instance prim_val_reflect_eq {term} {req : ReflectEq term} : ReflectEq (prim_val
   {| ReflectEq.eqb := eqb_prim_val (equ := eqb) (req := eqb) |}.
 Next Obligation.
   intros. funelim (eqb_prim_val x y); simp eqb_prim_val.
-  change (eqb_prim_model i i') with (eqb i i').
-  case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto.
-  constructor. intros H; noconf H; auto.
-  constructor. intros H; noconf H; auto.
-  constructor. intros H; noconf H; auto.
-  change (eqb_prim_model f f') with (eqb f f').
-  case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
-  constructor. intros H; noconf H; auto.
-  constructor. intros H; noconf H; auto.
-  constructor. intros H; noconf H; auto.
-  change (eqb_prim_model a a') with (eqb a a').
-  case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
+  all: try by constructor; intros H; noconf H; auto.
+  - change (eqb_prim_model i i') with (eqb i i').
+    case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto.
+  - change (eqb_prim_model f f') with (eqb f f').
+    case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
+  - change (eqb_prim_model s s') with (eqb s s').
+    case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
+  - change (eqb_prim_model a a') with (eqb a a').
+    case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
 Qed.
 
 #[global]
-Instance prim_tag_model_eqdec term {req : ReflectEq term} : EqDec (prim_val term) := _.
+  Instance prim_tag_model_eqdec term {req : ReflectEq term} : EqDec (prim_val term) := _.
 
 (** Printing *)
 
@@ -154,6 +172,7 @@ Definition string_of_prim {term} (soft : term -> string) (p : prim_val term) : s
   match p.π2 return string with
   | primIntModel f => "(int: " ^ string_of_prim_int f ^ ")"
   | primFloatModel f => "(float: " ^ string_of_float f ^ ")"
+  | primStringModel s => "(string: " ^ string_of_pstring s ^ ")"
   | primArrayModel a => "(array:" ^ string_of_list soft a.(array_value) ^ ")"
   end.
 
@@ -162,6 +181,7 @@ Definition string_of_prim {term} (soft : term -> string) (p : prim_val term) : s
 Inductive onPrim {term} (P : term -> Prop) : prim_val term -> Prop :=
   | onPrimInt i : onPrim P (primInt; primIntModel i)
   | onPrimFloat f : onPrim P (primFloat; primFloatModel f)
+  | onPrimString s : onPrim P (primString; primStringModel s)
   | onPrimArray a :
     P a.(array_default) ->
     P a.(array_type) ->
@@ -172,6 +192,7 @@ Derive Signature for onPrim.
 Inductive onPrims {term} (eq_term : term -> term -> Type) Re : prim_val term -> prim_val term -> Type :=
   | onPrimsInt i : onPrims eq_term Re (primInt; primIntModel i) (primInt; primIntModel i)
   | onPrimsFloat f : onPrims eq_term Re (primFloat; primFloatModel f) (primFloat; primFloatModel f)
+  | onPrimsString s : onPrims eq_term Re (primString; primStringModel s) (primString; primStringModel s)
   | onPrimsArray a a' :
     Re (Universe.make' a.(array_level)) (Universe.make' a'.(array_level)) ->
     eq_term a.(array_default) a'.(array_default) ->
@@ -184,6 +205,7 @@ Definition tPrimProp {term} (P : term -> Type) (p : PCUICPrimitive.prim_val term
   match p.π2 return Type with
   | primIntModel f => unit
   | primFloatModel f => unit
+  | primStringModel s => unit
   | primArrayModel a => P a.(array_type) × P a.(array_default) × All P a.(array_value)
   end.
 
@@ -191,6 +213,7 @@ Definition tPrimProp {term} (P : term -> Type) (p : PCUICPrimitive.prim_val term
 Inductive onPrims_dep {term} (eq_term : term -> term -> Type) (Re : Universe.t -> Universe.t -> Prop) (eq_term_dep : forall x y, eq_term x y -> Type) (Re' : forall a b, Re a b -> Type) : forall x y : prim_val term, onPrims eq_term Re x y -> Type :=
   | onPrimsInt_dep i : onPrims_dep eq_term Re eq_term_dep Re' (primInt; primIntModel i) (primInt; primIntModel i) (onPrimsInt eq_term Re i)
   | onPrimsFloat_dep f : onPrims_dep eq_term Re eq_term_dep Re' (primFloat; primFloatModel f) (primFloat; primFloatModel f) (onPrimsFloat _ _ f)
+  | onPrimsString_dep s : onPrims_dep eq_term Re eq_term_dep Re' (primString; primStringModel s) (primString; primStringModel s) (onPrimsString _ _ s)
   | onPrimsArray_dep a a' :
     forall (hre : Re (Universe.make' a.(array_level)) (Universe.make' a'.(array_level)))
     (eqdef : eq_term a.(array_default) a'.(array_default))
@@ -217,6 +240,7 @@ Equations mapu_prim {term term'} (f : Level.t -> Level.t) (g : term -> term')
   (p : PCUICPrimitive.prim_val term) : PCUICPrimitive.prim_val term' :=
 | _, _, (primInt; primIntModel i) => (primInt; primIntModel i)
 | _, _, (primFloat; primFloatModel fl) => (primFloat; primFloatModel fl)
+| _, _, (primString; primStringModel s) => (primString; primStringModel s)
 | f, g, (primArray; primArrayModel ar) =>
   (primArray; primArrayModel (mapu_array_model f g ar)).
 
@@ -226,12 +250,14 @@ Notation map_prim := (mapu_prim id).
 Equations test_prim {term} (p : term -> bool) (p : prim_val term) : bool :=
 | p, (primInt; _) => true
 | p, (primFloat; _) => true
+| p, (primString; _) => true
 | p, (primArray; primArrayModel ar) =>
   List.forallb p ar.(array_value) && p ar.(array_default) && p ar.(array_type).
 
 Equations test_primu {term} (p : Level.t -> bool) (t : term -> bool) (p : prim_val term) : bool :=
 | _, _, (primInt; _) => true
 | _, _, (primFloat; _) => true
+| _, _, (primString; _) => true
 | p, pt, (primArray; primArrayModel ar) =>
   p ar.(array_level) && forallb pt ar.(array_value) &&
   pt ar.(array_default) && pt ar.(array_type).
diff --git a/pcuic/theories/utils/PCUICSize.v b/pcuic/theories/utils/PCUICSize.v
index 3822c0b0d..0d62b37da 100644
--- a/pcuic/theories/utils/PCUICSize.v
+++ b/pcuic/theories/utils/PCUICSize.v
@@ -27,6 +27,7 @@ Definition prim_size (size : term -> nat) (p : prim_val) : nat :=
   match p.π2 return nat with
   | primIntModel f => 0
   | primFloatModel f => 0
+  | primStringModel s => 0
   | primArrayModel a => size a.(array_type) + size a.(array_default) + list_size size a.(array_value)
   end.
 
@@ -60,4 +61,4 @@ Proof.
   induction l in n |- *; destruct n; simpl => //; auto.
   - intros [= <-]. lia.
   - intros hnth. specialize (IHl _ hnth). lia.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v
index 2bc1f6380..bbb28c74a 100644
--- a/quotation/theories/CommonUtils.v
+++ b/quotation/theories/CommonUtils.v
@@ -188,6 +188,7 @@ Module WithTemplate.
          | tVar _
          | tInt _
          | tFloat _
+         | tString _
          | tArray _ _ _ _
          | tConst _ _
          | tInd _ _
diff --git a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
index eb1225ab6..d3244177a 100644
--- a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
+++ b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
@@ -17,6 +17,8 @@ From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall.
 
 #[export] Instance quote_prim_model {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model term tag) := ltac:(destruct 1; eauto).
 
+#[global] Instance quote_pstring : ground_quotable PrimString.string := fun s => PCUICAst.tString s.
+
 #[export] Instance quote_prim_model_of {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model_of term tag) := ltac:(cbv [prim_model_of]; destruct tag; exact _).
 
 #[export] Instance quote_prim_val {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_val term) := ltac:(cbv [prim_val]; exact _).
diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v
index bc994b34c..b0f730bc3 100644
--- a/quotation/theories/ToTemplate/Init.v
+++ b/quotation/theories/ToTemplate/Init.v
@@ -109,6 +109,7 @@ Proof.
      | tSort _
      | tInt _
      | tFloat _
+     | tString _
      | tArray _ _ _ _
      | tConst _ _
        => if head_term_is_bound cur_modpath qt
@@ -214,6 +215,7 @@ Proof.
        | tConstruct _ _ _
        | tInt _
        | tFloat _
+       | tString _
        | tArray _ _ _ _
        | tInd _ _
          => ret qt
diff --git a/quotation/theories/ToTemplate/Template/Ast.v b/quotation/theories/ToTemplate/Template/Ast.v
index 28de2e3df..925d6c009 100644
--- a/quotation/theories/ToTemplate/Template/Ast.v
+++ b/quotation/theories/ToTemplate/Template/Ast.v
@@ -6,6 +6,8 @@ From MetaCoq.Quotation.ToTemplate.Common Require Import Environment EnvironmentT
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig.
 From MetaCoq.Quotation.ToTemplate.QuotationOf.Template Require Import Ast.Instances ReflectAst.Instances.
 
+#[export] Instance quote_pstring : ground_quotable PrimString.string := fun s => Ast.tString s.
+
 #[export] Instance quote_predicate {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (predicate term) := ltac:(destruct 1; exact _).
 #[export] Instance quote_branch {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (branch term) := ltac:(destruct 1; exact _).
 #[local] Hint Extern 1 => assumption : typeclass_instances.
diff --git a/safechecker/theories/PCUICEqualityDec.v b/safechecker/theories/PCUICEqualityDec.v
index 9980add1c..40014fa3b 100644
--- a/safechecker/theories/PCUICEqualityDec.v
+++ b/safechecker/theories/PCUICEqualityDec.v
@@ -520,7 +520,7 @@ Proof.
     cbn in X, ht, ht';
     rewrite /eqb_prim_val /eqb_prim_model; cbn -[eqb]; try eqspecs;
     try repeat constructor.
-    1-8:intros e; depelim e; try depelim o; intuition eauto.
+    1-15:intros e; depelim e; try depelim o; intuition eauto.
     rtoProp. destruct X as (hty & hdef & harr).
     eapply reflectT_change_left. { split; intros XE. 1: constructor; now apply XE. now depelim XE. }
     eapply reflectT_change_left4. { split; intros XE. 1: destruct XE as [XE1 XE2 XE3 XE4]; constructor; [apply XE1|apply XE3|apply XE4|apply XE2]. now depelim XE. }
diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v
index 4c294d059..a4ebfc55a 100644
--- a/safechecker/theories/PCUICSafeConversion.v
+++ b/safechecker/theories/PCUICSafeConversion.v
@@ -3586,6 +3586,9 @@ Equations (noeqns) isconv_array_values_aux
         | (primFloat; primFloatModel f) | (primFloat; primFloatModel f') with inspect (eqb f f') :=
           { | @exist true eqf := yes
             | @exist false neqf := no (DistinctPrimValues (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') }
+        | (primString; primStringModel f) | (primString; primStringModel f') with inspect (eqb f f') :=
+          { | @exist true eqf := yes
+            | @exist false neqf := no (DistinctPrimValues (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') }
         | (primArray; primArrayModel a) | (primArray; primArrayModel a')
           with inspect (abstract_env_compare_universe X Conv (Universe.make' (array_level a)) (Universe.make' (array_level a'))) :=
           { | @exist false neql := no (ArrayNotConvertibleLevels (Γ ,,, stack_context π1) a (Γ ,,, stack_context π2) a')
@@ -4765,6 +4768,44 @@ Qed.
     now rewrite eqb_refl in neqf.
   Qed.
 
+  Next Obligation.
+  Proof.
+    symmetry in eqf.
+    apply eqb_eq in eqf; subst f'.
+    rename H into wfΣ. pose proof (hΣ _ wfΣ) as [hΣ].
+    clear aux.
+    specialize (hx Σ wfΣ).
+    specialize (h1 Σ wfΣ).
+    specialize (h2 Σ wfΣ).
+    apply welltyped_zipc_zipp in h1; eauto.
+    eapply welltyped_zipc_zipp in h2; eauto.
+    rewrite !zipp_as_mkApps in h1, h2 |- *.
+    apply mkApps_Prim_nil in h1; auto.
+    apply mkApps_Prim_nil in h2; auto.
+    rewrite h1 h2; cbn.
+    red. sq. eapply ws_cumul_pb_Prim; eauto; fvs.
+    constructor.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
+    pose proof (hΣ _ wfΣ) as [hΣ].
+    specialize (H _ wfΣ).
+    specialize (hx Σ wfΣ).
+    specialize (h1 Σ wfΣ).
+    apply welltyped_zipc_zipp in h1; eauto.
+    clear aux.
+    eapply welltyped_zipc_zipp in h2; eauto.
+    rewrite !zipp_as_mkApps in h1, h2, H |- *.
+    apply mkApps_Prim_nil in h1; auto.
+    apply mkApps_Prim_nil in h2; auto.
+    rewrite h1 h2 in H.
+    destruct H as [H]. cbn in H.
+    eapply invert_cumul_Prim in H; depelim H.
+    now rewrite eqb_refl in neqf.
+  Qed.
+
   Next Obligation.
   Proof.
     destruct a; eauto.
diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v
index 75d642aaf..b968cc1bc 100644
--- a/safechecker/theories/PCUICTypeChecker.v
+++ b/safechecker/theories/PCUICTypeChecker.v
@@ -1318,6 +1318,11 @@ Section Typecheck.
       check_eq_true (eqb decl.(cst_universes) Monomorphic_ctx) (Msg "primitive type for floats is registered to non-monomorphic constant") ;;
       check_eq_true (eqb decl.(cst_type) (tSort Sort.type0)) (Msg "primitive type for floats is registered to an axiom whose type is not the sort Set") ;;
       ret _
+  | primString | decl :=
+                  check_eq_true (eqb decl.(cst_body) None) (Msg "primitive type is registered to a defined constant") ;;
+                  check_eq_true (eqb decl.(cst_universes) Monomorphic_ctx) (Msg "primitive type for strings is registered to non-monomorphic constant") ;;
+                  check_eq_true (eqb decl.(cst_type) (tSort Sort.type0)) (Msg "primitive type for strings is registered to an axiom whose type is not the sort Set") ;;
+                  ret _
    | primArray | decl :=
       let s := sType (Universe.make' (Level.lvar 0)) in
       check_eq_true (eqb decl.(cst_body) None) (Msg "primitive type is registered to a defined constant") ;;
@@ -1328,15 +1333,7 @@ Section Typecheck.
     all:try eapply eqb_eq in i.
     all:try apply eqb_eq in i0.
     all:try apply eqb_eq in i1 => //.
-    - destruct H as []. rewrite H in absurd; eauto.
-    - destruct H as []. apply absurd. now rewrite H1; apply eqb_refl.
-    - destruct H as []. apply absurd; rewrite H0; apply eqb_refl.
-    - destruct H as []. rewrite H in absurd; eauto.
-    - destruct H as []. apply absurd. now rewrite H1; apply eqb_refl.
-    - destruct H as []. apply absurd; rewrite H0; apply eqb_refl.
-    - destruct H as []. rewrite H in absurd; eauto.
-    - destruct H as []. apply absurd. now rewrite H1; apply eqb_refl.
-    - destruct H as []. apply absurd; rewrite H0; apply eqb_refl.
+    all:destruct H as []; apply absurd; rewrite ?H ?H0 ?H1; eauto.
   Qed.
 
   Section make_All.
@@ -1362,6 +1359,7 @@ Section Typecheck.
     Equations? check_primitive_typing (p : prim_val) : typing_result_comp (forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ primitive_typing_hyps checking Σ Γ p ∥) :=
       | (primInt; primIntModel i) := ret _
       | (primFloat; primFloatModel f) := ret _
+      | (primString; primStringModel f) := ret _
       | (primArray; primArrayModel a) :=
         check_eq_true (abstract_env_ext_wf_universeb X (Universe.make' a.(array_level))) (Msg "primitive array level is not well-formed") ;;
         check_type <- bdcheck infer Γ wfΓ a.(array_type) (tSort (sType (Universe.make' a.(array_level)))) _ ;;
@@ -1372,7 +1370,7 @@ Section Typecheck.
       all:intros.
       all:try pose proof (abstract_env_ext_wf _ wfΣ) as [wfΣ'].
       all:try specialize (wfΓ _ wfΣ).
-      1-2:do 2 constructor.
+      1-3:do 2 constructor.
       - eauto.
       - sq. erewrite <- abstract_env_ext_wf_universeb_correct in i; tea.
         eapply has_sort_isType; eapply type_Sort; eauto.
diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject
index 314e020ac..b1fc2531f 100644
--- a/template-coq/_PluginProject
+++ b/template-coq/_PluginProject
@@ -195,8 +195,12 @@ gen-src/primFloat.ml
 gen-src/primFloat.mli
 gen-src/primInt63.ml
 gen-src/primInt63.mli
+gen-src/primString.ml
+gen-src/primString.mli
 gen-src/primitive.ml
 gen-src/primitive.mli
+gen-src/pString.ml
+gen-src/pString.mli
 gen-src/quoter.ml
 gen-src/reflect.ml
 gen-src/reflect.mli
diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in
index dcecb5541..740a83958 100644
--- a/template-coq/_PluginProject.in
+++ b/template-coq/_PluginProject.in
@@ -193,8 +193,12 @@ gen-src/primFloat.ml
 gen-src/primFloat.mli
 gen-src/primInt63.ml
 gen-src/primInt63.mli
+gen-src/primString.ml
+gen-src/primString.mli
 gen-src/primitive.ml
 gen-src/primitive.mli
+gen-src/pString.ml
+gen-src/pString.mli
 gen-src/quoter.ml
 gen-src/reflect.ml
 gen-src/reflect.mli
diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack
index 78da99ee2..0f93f7515 100644
--- a/template-coq/gen-src/metacoq_template_plugin.mlpack
+++ b/template-coq/gen-src/metacoq_template_plugin.mlpack
@@ -74,6 +74,8 @@ Zpower
 SpecFloat
 PrimFloat
 FloatOps
+PrimString
+PString
 MCString
 Sint63
 Show
diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml
index f5f349413..4accda36a 100644
--- a/template-coq/src/ast_denoter.ml
+++ b/template-coq/src/ast_denoter.ml
@@ -13,6 +13,7 @@ struct
   type quoted_int = Datatypes.nat
   type quoted_int63 = Uint63.t
   type quoted_float64 = Float64.t
+  type quoted_pstring = Pstring.t
   type quoted_bool = bool
   type quoted_name = name
   type quoted_aname = name binder_annot
@@ -104,7 +105,7 @@ struct
 
   let inspect_term (tt: t):(t, quoted_int, quoted_ident, quoted_aname, quoted_sort, quoted_cast_kind,
     quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj,
-    quoted_int63, quoted_float64) structure_of_term =
+    quoted_int63, quoted_float64, quoted_pstring) structure_of_term =
     match tt with
     | Coq_tRel n -> ACoq_tRel n
     | Coq_tVar v -> ACoq_tVar v
@@ -125,6 +126,7 @@ struct
     | Coq_tCoFix (a,b) -> ACoq_tCoFix (List.map unquote_def a,b)
     | Coq_tInt i -> ACoq_tInt i
     | Coq_tFloat f -> ACoq_tFloat f
+    | Coq_tString s -> ACoq_tString s
     | Coq_tArray (u, arr, def, ty) -> ACoq_tArray (u, Array.of_list arr, def, ty)
 
   let unquote_string = Caml_bytestring.caml_string_of_bytestring
@@ -161,6 +163,8 @@ struct
 
   let unquote_float64 i = i
 
+  let unquote_pstring s = s
+
   (* val unquote_sort : quoted_sort -> Sorts.t *)
   (* val unquote_sort_family : quoted_sort_family -> Sorts.family *)
   let unquote_cast_kind (q : quoted_cast_kind) : Constr.cast_kind =
diff --git a/template-coq/src/ast_quoter.ml b/template-coq/src/ast_quoter.ml
index bae47d447..b287cf827 100644
--- a/template-coq/src/ast_quoter.ml
+++ b/template-coq/src/ast_quoter.ml
@@ -14,6 +14,7 @@ struct
   type quoted_int = Datatypes.nat
   type quoted_int63 = Uint63.t
   type quoted_float64 = Float64.t
+  type quoted_pstring = Pstring.t
   type quoted_bool = bool
   type quoted_name = BasicAst.name
   type quoted_aname = BasicAst.aname
@@ -80,6 +81,8 @@ struct
 
   let quote_float64 x = x
 
+  let quote_pstring x = x
+
   let quote_level (l : Univ.Level.t) : Universes0.Level.t =
     if Univ.Level.is_set l then Universes0.Level.Coq_lzero
     else match Univ.Level.var_index l with
@@ -240,6 +243,7 @@ struct
   let mkLetIn na b t t' = Coq_tLetIn (na,b,t,t')
   let mkInt i = Coq_tInt i
   let mkFloat f = Coq_tFloat f
+  let mkString s = Coq_tString s
   let mkArray u arr ~default ~ty = Coq_tArray (u, Array.to_list arr, default, ty)
 
   let rec seq f t =
@@ -320,11 +324,13 @@ struct
   type pre_quoted_retroknowledge =
     { retro_int63 : quoted_kernel_name option;
       retro_float64 : quoted_kernel_name option;
+      retro_string : quoted_kernel_name option;
       retro_array : quoted_kernel_name option }
 
   let quote_retroknowledge r =
     { Environment.Retroknowledge.retro_int63 = r.retro_int63;
       Environment.Retroknowledge.retro_float64 = r.retro_float64;
+      Environment.Retroknowledge.retro_string = r.retro_string;
       Environment.Retroknowledge.retro_array = r.retro_array }
 
   let mk_global_env universes declarations retroknowledge = { universes; declarations; retroknowledge }
@@ -376,7 +382,7 @@ struct
   let inspectTerm (t : term) :  (term, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind,
     quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level,
     quoted_univ_instance, quoted_proj,
-    quoted_int63, quoted_float64) structure_of_term =
+    quoted_int63, quoted_float64, quoted_pstring) structure_of_term =
    match t with
   | Coq_tRel n -> ACoq_tRel n
   (* todo ! *)
diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml
index a8095b373..c0cbc21e4 100644
--- a/template-coq/src/constr_denoter.ml
+++ b/template-coq/src/constr_denoter.ml
@@ -79,6 +79,11 @@ struct
     | Constr.Float f -> f
     | _ -> not_supported_verb trm "unquote_float64"
 
+  let unquote_pstring trm =
+    match Constr.kind trm with
+    | Constr.String s -> s
+    | _ -> not_supported_verb trm "unquote_pstring"
+
   let unquote_char trm =
     let (h,args) = app_full trm [] in
     match Constr.kind h with
@@ -378,7 +383,7 @@ struct
   let inspect_term (t:Constr.t)
   : (Constr.t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name,
     quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj,
-    quoted_int63, quoted_float64) structure_of_term =
+    quoted_int63, quoted_float64, quoted_pstring) structure_of_term =
     (* debug (fun () -> Pp.(str "denote_term" ++ spc () ++ print_term t)) ; *)
     let (h,args) = app_full t [] in
     if constr_equall h tRel then
@@ -480,6 +485,10 @@ struct
       match args with
         t::_ -> ACoq_tFloat t
       | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
+    else if constr_equall h tString then
+      match args with
+        t::_ -> ACoq_tString t
+      | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure"))
     else if constr_equall h tArray then
       match args with
         u::v::def::ty::_ -> ACoq_tArray (u, Array.of_list (unquote_list v), def, ty)
diff --git a/template-coq/src/constr_quoter.ml b/template-coq/src/constr_quoter.ml
index 24c317e04..fff2a8d20 100644
--- a/template-coq/src/constr_quoter.ml
+++ b/template-coq/src/constr_quoter.ml
@@ -95,6 +95,7 @@ struct
 
   let mkInt i = i
   let mkFloat f = f
+  let mkString s = s
 
   let mkArray u arr ~default ~ty =
     constr_mkApp (tArray, [| u; to_coq_listl tTerm (Array.to_list arr); default; ty |])
@@ -129,6 +130,9 @@ struct
   let quote_int63 i = constr_mkApp (tInt, [| Constr.mkInt i |])
 
   let quote_float64 f = constr_mkApp (tFloat, [| Constr.mkFloat f |])
+
+  let quote_pstring s = constr_mkApp (tString, [| Constr.mkString s |])
+
   let quote_inductive (kn, i) =
     constr_mkApp (tmkInd, [| kn; i |])
 
@@ -423,13 +427,15 @@ struct
   type pre_quoted_retroknowledge =
     { retro_int63 : quoted_kernel_name option;
       retro_float64 : quoted_kernel_name option;
+      retro_string : quoted_kernel_name option;
       retro_array : quoted_kernel_name option }
 
   let quote_retroknowledge r =
     let rint63 = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_int63 in
     let rfloat64 = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_float64 in
+    let rstring = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_string in
     let rarray = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_array in
-    constr_mkApp (tmk_retroknowledge, [| rint63; rfloat64; rarray |])
+    constr_mkApp (tmk_retroknowledge, [| rint63; rfloat64; rstring; rarray |])
 
   let mk_global_env univs decls retro =
     constr_mkApp (tBuild_global_env, [| univs; decls; retro |])
diff --git a/template-coq/src/constr_reification.ml b/template-coq/src/constr_reification.ml
index ff8c9f665..c590bb610 100644
--- a/template-coq/src/constr_reification.ml
+++ b/template-coq/src/constr_reification.ml
@@ -17,6 +17,7 @@ struct
   type quoted_proj = Constr.t (* of type Ast.projection *)
   type quoted_int63 = Constr.t (* of type UInt63.t *)
   type quoted_float64 = Constr.t (* of type Float64.t *)
+  type quoted_pstring = Constr.t (* of type Float64.t *)
   type quoted_global_reference = Constr.t (* of type Ast.global_reference *)
 
   type quoted_sort_family = Constr.t (* of type Ast.sort_family *)
diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml
index f84405bc4..5e4bcdfb2 100644
--- a/template-coq/src/denoter.ml
+++ b/template-coq/src/denoter.ml
@@ -15,6 +15,7 @@ sig
   val unquote_bool : quoted_bool -> bool
   val unquote_int63 : quoted_int63 -> Uint63.t
   val unquote_float64 : quoted_float64 -> Float64.t
+  val unquote_pstring : quoted_pstring -> Pstring.t
   val unquote_cast_kind : quoted_cast_kind -> Constr.cast_kind
   val unquote_kn :  quoted_kernel_name -> KerName.t
   val unquote_inductive :  quoted_inductive -> Names.inductive
@@ -28,7 +29,7 @@ sig
   (* val representsIndConstuctor : quoted_inductive -> Term.constr -> bool *)
   val inspect_term : t -> (t, quoted_int, quoted_ident, quoted_aname, quoted_sort, quoted_cast_kind,
     quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj,
-    quoted_int63, quoted_float64) structure_of_term
+    quoted_int63, quoted_float64, quoted_pstring) structure_of_term
 
 end
 
@@ -165,6 +166,7 @@ struct
          evm, Constr.mkProj (p', r, t')
       | ACoq_tInt x -> evm, Constr.mkInt (D.unquote_int63 x)
       | ACoq_tFloat x -> evm, Constr.mkFloat (D.unquote_float64 x)
+      | ACoq_tString x -> evm, Constr.mkString (D.unquote_pstring x)
       | ACoq_tArray (u, arr, def, ty) ->
           let evm, u = D.unquote_universe_level evm u in
           let evm, arr = CArray.fold_left_map (fun evm a -> aux env evm a) evm arr in
diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
index a523f3367..6b2bc9630 100644
--- a/template-coq/src/quoter.ml
+++ b/template-coq/src/quoter.ml
@@ -85,6 +85,7 @@ sig
   val mkCoFix : (quoted_int array * quoted_int) * (quoted_aname array * t array * t array) -> t
   val mkInt : quoted_int63 -> t
   val mkFloat : quoted_float64 -> t
+  val mkString : quoted_pstring -> t
   val mkArray : quoted_univ_level -> t array -> default:t -> ty:t -> t
 
   val mkBindAnn : quoted_name -> quoted_relevance -> quoted_aname
@@ -107,6 +108,7 @@ sig
   (* Primitive objects *)
   val quote_int63 : Uint63.t -> quoted_int63
   val quote_float64 : Float64.t -> quoted_float64
+  val quote_pstring : Pstring.t -> quoted_pstring
 
   val quote_constraint_type : Univ.constraint_type -> quoted_constraint_type
   val quote_univ_constraint : Univ.univ_constraint -> quoted_univ_constraint
@@ -174,6 +176,7 @@ sig
   type pre_quoted_retroknowledge =
     { retro_int63 : quoted_kernel_name option;
       retro_float64 : quoted_kernel_name option;
+      retro_string : quoted_kernel_name option;
       retro_array : quoted_kernel_name option }
 
   val quote_retroknowledge : pre_quoted_retroknowledge -> quoted_retroknowledge
@@ -359,6 +362,7 @@ struct
          (Q.mkProj p' t', add_inductive (Projection.inductive p) mib acc)
       | Constr.Int i -> (Q.mkInt (Q.quote_int63 i), acc)
       | Constr.Float f -> (Q.mkFloat (Q.quote_float64 f), acc)
+      | Constr.String s -> (Q.mkString (Q.quote_pstring s), acc)
       | Constr.Meta _ -> failwith "Meta not supported by TemplateCoq"
       | Constr.Array (u, ar, def, ty) ->
         let u = match UVars.Instance.to_array u with (_, [| u |]) -> u | _ -> assert false in
@@ -610,6 +614,7 @@ struct
       let pre =
         { Q.retro_int63 = quote_retro retro.Retroknowledge.retro_int63 ;
           Q.retro_float64 = quote_retro retro.Retroknowledge.retro_float64 ;
+          Q.retro_string = quote_retro retro.Retroknowledge.retro_string ;
           Q.retro_array = quote_retro retro.Retroknowledge.retro_array }
       in Q.quote_retroknowledge pre
     in
diff --git a/template-coq/src/reification.ml b/template-coq/src/reification.ml
index 5eae5f27e..1f5e77788 100644
--- a/template-coq/src/reification.ml
+++ b/template-coq/src/reification.ml
@@ -16,6 +16,7 @@ sig
   type quoted_proj
   type quoted_int63
   type quoted_float64
+  type quoted_pstring
 
   type quoted_global_reference
 
diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml
index 6a13c0cb0..aef445e47 100644
--- a/template-coq/src/tm_util.ml
+++ b/template-coq/src/tm_util.ml
@@ -338,7 +338,7 @@ type ('nat, 'inductive, 'relevance) acase_info =
     aci_npar : 'nat;
     aci_relevance : 'relevance }
 
-type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'relevance, 'universe_level, 'universe_instance, 'projection, 'int63, 'float64) structure_of_term =
+type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'relevance, 'universe_level, 'universe_instance, 'projection, 'int63, 'float64, 'pstring) structure_of_term =
   | ACoq_tRel of 'nat
   | ACoq_tVar of 'ident
   | ACoq_tEvar of 'nat * 'term list
@@ -359,5 +359,6 @@ type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive
   | ACoq_tCoFix of ('term, 'name, 'nat) amfixpoint * 'nat
   | ACoq_tInt of 'int63
   | ACoq_tFloat of 'float64
+  | ACoq_tString of 'pstring
   | ACoq_tArray of 'universe_level * 'term array * 'term * 'term
 
diff --git a/template-coq/theories/Ast.v b/template-coq/theories/Ast.v
index c29d1e03b..a892e9228 100644
--- a/template-coq/theories/Ast.v
+++ b/template-coq/theories/Ast.v
@@ -3,7 +3,7 @@ From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Export Environment EnvironmentTyping Universes BasicAst.
 (* For primitive integers and floats  *)
-From Coq Require Uint63 Floats.PrimFloat Floats.SpecFloat PArray.
+From Coq Require Uint63 Floats.PrimFloat Floats.SpecFloat PArray PrimString.
 From Coq Require Import ssreflect Morphisms.
 
 (** * AST of Coq kernel terms and kernel data structures
@@ -416,6 +416,7 @@ Inductive term : Type :=
 | tCoFix (mfix : mfixpoint term) (idx : nat)
 | tInt (i : PrimInt63.int)
 | tFloat (f : PrimFloat.float)
+| tString (s : PrimString.string)
 | tArray (u : Level.t) (arr : list term) (default : term) (type : term).
 
 (** This can be used to represent holes, that, when unquoted, turn into fresh existential variables.
@@ -565,7 +566,7 @@ Fixpoint noccur_between k n (t : term) : bool :=
   fix subst_instance_constr u c {struct c} : term :=
   match c with
   | tRel _ | tVar _ => c
-  | tInt _ | tFloat _ => c
+  | tInt _ | tFloat _ | tString _ => c
   | tArray u' arr def ty => tArray (subst_instance_level u u') (List.map (subst_instance_constr u) arr)
     (subst_instance_constr u def) (subst_instance_constr u ty)
   | tEvar ev args => tEvar ev (List.map (subst_instance_constr u) args)
diff --git a/template-coq/theories/AstUtils.v b/template-coq/theories/AstUtils.v
index f0776280c..13a19a57b 100644
--- a/template-coq/theories/AstUtils.v
+++ b/template-coq/theories/AstUtils.v
@@ -68,6 +68,7 @@ Module string_of_term_tree.
   | tCoFix l n => "CoFix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")"
   | tInt i => "Int(" ^ string_of_prim_int i ^ ")"
   | tFloat f => "Float(" ^ string_of_float f ^ ")"
+  | tString s => "String(" ^ string_of_pstring s ^ ")"
   | tArray u arr def ty => "Array(" ^ string_of_level u ^ "," ^
     string_of_list string_of_term arr ^ "," ^ string_of_term def ^ "," ^ string_of_term ty ^ ")"
   end.
@@ -257,7 +258,7 @@ Fixpoint strip_casts t :=
   | tArray u arr def ty =>
     tArray u (List.map strip_casts arr) (strip_casts def) (strip_casts ty)
   | tRel _ | tVar _ | tSort _ | tConst _ _ | tInd _ _ | tConstruct _ _ _ => t
-  | tInt _ | tFloat _ => t
+  | tInt _ | tFloat _ | tString _ => t
   end.
 
 Fixpoint decompose_prod_assum (Γ : context) (t : term) : context * term :=
diff --git a/template-coq/theories/Checker.v b/template-coq/theories/Checker.v
index 6b5c7b1fc..128511517 100644
--- a/template-coq/theories/Checker.v
+++ b/template-coq/theories/Checker.v
@@ -800,7 +800,7 @@ Section Typecheck.
       | None => raise (IllFormedFix mfix n)
       end
 
-    | tInt _ | tFloat _ | tArray _ _ _ _ => raise (NotSupported "primitive types")
+    | tInt _ | tFloat _ | tString _ | tArray _ _ _ _ => raise (NotSupported "primitive types")
     end.
 
   Definition check (Γ : context) (t : term) (ty : term) : typing_result unit :=
diff --git a/template-coq/theories/EtaExpand.v b/template-coq/theories/EtaExpand.v
index 7e9c2b03b..a36212f92 100644
--- a/template-coq/theories/EtaExpand.v
+++ b/template-coq/theories/EtaExpand.v
@@ -138,7 +138,7 @@ Section Eta.
         end
     | tCast t1 k t2 => tCast (eta_expand Γ t1) k (eta_expand Γ t2)
     | tArray u arr def ty => tArray u (List.map (eta_expand Γ) arr) (eta_expand Γ def) (eta_expand Γ ty)
-    | tInt _ | tFloat _ => t
+    | tInt _ | tFloat _ | tString _ => t
     end.
 
 End Eta.
@@ -294,6 +294,7 @@ Inductive expanded (Γ : list nat): term -> Prop :=
     expanded Γ (tApp (tConstruct ind c u) args)
 | expanded_tInt i : expanded Γ (tInt i)
 | expanded_tFloat f : expanded Γ (tFloat f)
+| expanded_tString s : expanded Γ (tString s)
 | expanded_tArray u arr def ty :
   Forall (expanded Γ) arr ->
   expanded Γ def ->
@@ -363,6 +364,7 @@ forall (Σ : global_env) (P : list nat -> term -> Prop),
  P Γ(tApp (tConstruct ind c u) args)) ->
 (forall Γ i, P Γ (tInt i)) ->
 (forall Γ f, P Γ (tFloat f)) ->
+(forall Γ s, P Γ (tString s)) ->
 (forall Γ u arr def ty,
   Forall (P Γ) arr ->
   P Γ def ->
@@ -370,7 +372,7 @@ forall (Σ : global_env) (P : list nat -> term -> Prop),
   P Γ (tArray u arr def ty)) ->
  forall Γ, forall t : term, expanded Σ Γ t -> P Γ t.
 Proof.
-  intros Σ P HRel HRel_app HVar HEvar HSort HCast HProd HLamdba HLetIn HApp HConst HInd HConstruct HCase HProj HFix HCoFix HConstruct_app Hint Hfloat Harr.
+  intros Σ P HRel HRel_app HVar HEvar HSort HCast HProd HLamdba HLetIn HApp HConst HInd HConstruct HCase HProj HFix HCoFix HConstruct_app Hint Hfloat Hstring Harr.
   fix f 3.
   intros Γ t Hexp.  destruct Hexp; eauto.
   all: match goal with [H : Forall _ _ |- _] => let all := fresh "all" in rename H into all end.
diff --git a/template-coq/theories/Extraction.v b/template-coq/theories/Extraction.v
index 2315f833f..9af1bba3f 100644
--- a/template-coq/theories/Extraction.v
+++ b/template-coq/theories/Extraction.v
@@ -10,7 +10,7 @@ From Coq Require Ascii Extraction ZArith NArith.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import Reflect config.
 From MetaCoq.Template Require Import Ast Induction.
-From Coq Require Import FSets ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63.
+From Coq Require Import FSets ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63 ExtrOCamlPString.
 
 Extract Inductive Equations.Init.sigma => "( * )" ["(,)"].
 Extract Constant Equations.Init.pr1 => "fst".
diff --git a/template-coq/theories/Induction.v b/template-coq/theories/Induction.v
index d484cef7c..cabd504fb 100644
--- a/template-coq/theories/Induction.v
+++ b/template-coq/theories/Induction.v
@@ -34,6 +34,7 @@ Lemma term_forall_list_ind :
     (forall (m : mfixpoint term) (n : nat), tFixProp P P m -> P (tCoFix m n)) ->
     (forall i, P (tInt i)) ->
     (forall f, P (tFloat f)) ->
+    (forall s, P (tString s)) ->
     (forall u arr def ty, Forall P arr -> P def -> P ty -> P (tArray u arr def ty)) ->
     forall t : term, P t.
 Proof.
@@ -78,6 +79,7 @@ Lemma term_forall_list_rect :
     (forall (m : mfixpoint term) (n : nat), tFixType P P m -> P (tCoFix m n)) ->
     (forall i, P (tInt i)) ->
     (forall f, P (tFloat f)) ->
+    (forall s, P (tString s)) ->
     (forall u arr def ty, All P arr -> P def -> P ty -> P (tArray u arr def ty)) ->
     forall t : term, P t.
 Proof.
diff --git a/template-coq/theories/Pretty.v b/template-coq/theories/Pretty.v
index 2a16201f6..eb0171d30 100644
--- a/template-coq/theories/Pretty.v
+++ b/template-coq/theories/Pretty.v
@@ -252,6 +252,7 @@ Module PrintTermTree.
                               " in " ^ List.nth_default (string_of_nat n) (map (string_of_name ∘ binder_name ∘ dname) l) n)
   | tInt i => "Int(" ^ string_of_prim_int i ^ ")"
   | tFloat f => "Float(" ^ string_of_float f ^ ")"
+  | tString s => "Float(" ^ string_of_pstring s ^ ")"
   | tArray u arr def ty => "Array(" ^ string_of_level u ^ "," ^
     string_of_list string_of_term arr ^ "," ^ string_of_term def ^ "," ^ string_of_term ty ^ ")"
   end.
diff --git a/template-coq/theories/ReflectAst.v b/template-coq/theories/ReflectAst.v
index f2decc81a..283fcb460 100644
--- a/template-coq/theories/ReflectAst.v
+++ b/template-coq/theories/ReflectAst.v
@@ -57,6 +57,14 @@ Defined.
 
 Derive NoConfusion NoConfusionHom for term.
 
+#[global] Instance EqDec_pstring : EqDec PrimString.string.
+Proof.
+  intros s1 s2. destruct (PrimString.compare s1 s2) eqn:Hcmp; [left|right|right].
+  - by apply PString.string_eq_spec.
+  - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. discriminate Hcmp.
+  - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. discriminate Hcmp.
+Qed.
+
 #[global] Instance EqDec_term : EqDec term.
 Proof.
   intro x; induction x using term_forall_list_rect ; intro t ;
@@ -158,6 +166,8 @@ Proof.
     subst. left. reflexivity.
   - destruct (eq_dec f f0) ; nodec.
     subst. left. reflexivity.
+  - destruct (eq_dec s s0) ; nodec.
+    subst. left. reflexivity.
   - destruct (IHx1 t1); subst; nodec.
     destruct (IHx2 t2); subst; nodec.
     destruct (eq_dec u u0); nodec; subst.
diff --git a/template-coq/theories/TermEquality.v b/template-coq/theories/TermEquality.v
index a6cb5f424..d37bd614c 100644
--- a/template-coq/theories/TermEquality.v
+++ b/template-coq/theories/TermEquality.v
@@ -296,6 +296,7 @@ Inductive eq_term_upto_univ_napp Σ
 
 | eq_Int i : eq_term_upto_univ_napp Σ cmp_universe cmp_sort pb napp (tInt i) (tInt i)
 | eq_Float f : eq_term_upto_univ_napp Σ cmp_universe cmp_sort pb napp (tFloat f) (tFloat f)
+| eq_String s : eq_term_upto_univ_napp Σ cmp_universe cmp_sort pb napp (tString s) (tString s)
 | eq_Array u u' arr arr' def def' ty ty' :
   cmp_universe_instance (cmp_universe Conv) [u] [u'] ->
   All2 (eq_term_upto_univ_napp Σ cmp_universe cmp_sort Conv 0) arr arr' ->
diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v
index 24a8e6682..055c2f289 100644
--- a/template-coq/theories/Typing.v
+++ b/template-coq/theories/Typing.v
@@ -879,6 +879,13 @@ Inductive typing `{checker_flags} (Σ : global_env_ext) (Γ : context) : term ->
     primitive_invariants primFloat cdecl ->
     Σ ;;; Γ |- tFloat p : tConst prim_ty []
 
+| type_String p prim_ty cdecl :
+  wf_local Σ Γ ->
+  primitive_constant Σ primString = Some prim_ty ->
+  declared_constant Σ prim_ty cdecl ->
+  primitive_invariants primString cdecl ->
+  Σ ;;; Γ |- tString p : tConst prim_ty []
+
 | type_Array prim_ty cdecl u arr def ty :
     wf_local Σ Γ ->
     primitive_constant Σ primArray = Some prim_ty ->
@@ -1009,6 +1016,7 @@ Proof.
       (all_size (on_def_body (lift_typing typing _) _ _) (fun x p => on_def_body_size (typing_size Σ) _ _ _ p) a1))).
   - exact (S (All_local_env_size (typing_size _) _ a)).
   - exact (S (All_local_env_size (typing_size _) _ a)).
+  - exact (S (All_local_env_size (typing_size _) _ a)).
   - exact (S (Nat.max (All_local_env_size (typing_size _) _ a) (Nat.max d2 (Nat.max d3 (all_size _ (fun t p => typing_size Σ Γ t ty p) a0))))).
 Defined.
 
@@ -1285,6 +1293,13 @@ Lemma typing_ind_env `{cf : checker_flags} :
         primitive_invariants primFloat cdecl ->
         P Σ Γ (tFloat p) (tConst prim_ty [])) ->
 
+    (forall Σ (wfΣ : wf Σ) (Γ : context) (wfΓ : wf_local Σ Γ) p prim_ty cdecl,
+        PΓ Σ Γ wfΓ ->
+        primitive_constant Σ primString = Some prim_ty ->
+        declared_constant Σ prim_ty cdecl ->
+        primitive_invariants primString cdecl ->
+        P Σ Γ (tString p) (tConst prim_ty [])) ->
+
     (forall Σ (wfΣ : wf Σ) (Γ : context) (wfΓ : wf_local Σ Γ) u arr def ty prim_ty cdecl,
         PΓ Σ Γ wfΓ ->
         primitive_constant Σ primArray = Some prim_ty ->
@@ -1311,7 +1326,7 @@ Lemma typing_ind_env `{cf : checker_flags} :
 Proof.
   intros P Pj Pdecl PΓ; unfold env_prop.
   intros Xj XΓ.
-  intros X X0 Xcast X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 Xint Xfloat Xarr X12 Σ wfΣ Γ wfΓ t T H.
+  intros X X0 Xcast X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 Xint Xfloat Xstring Xarr X12 Σ wfΣ Γ wfΓ t T H.
   (* NOTE (Danil): while porting to 8.9, I had to split original "pose" into 2 pieces,
    otherwise it takes forever to execure the "pose", for some reason *)
   pose (@Fix_F ({ Σ : global_env_ext & { wfΣ : wf Σ & { Γ & { t & { T & Σ ;;; Γ |- t : T }}}}})) as p0.
diff --git a/template-coq/theories/WfAst.v b/template-coq/theories/WfAst.v
index cf6739816..d2a757eed 100644
--- a/template-coq/theories/WfAst.v
+++ b/template-coq/theories/WfAst.v
@@ -58,6 +58,7 @@ Inductive wf {Σ} : term -> Type :=
 | wf_tCoFix mfix k : All (fun def => wf def.(dtype) × wf def.(dbody)) mfix -> wf (tCoFix mfix k)
 | wf_tInt i : wf (tInt i)
 | wf_tFloat f : wf (tFloat f)
+| wf_tString s : wf (tString s)
 | wf_tArray u arr def ty : All wf arr -> wf def -> wf ty -> wf (tArray u arr def ty).
 Arguments wf : clear implicits.
 Derive Signature for wf.
@@ -67,7 +68,7 @@ Derive Signature for wf.
 Definition wf_Inv Σ (t : term) : Type :=
   match t with
   | tRel _ | tVar _ | tSort _ => unit
-  | tInt _ | tFloat _ => unit
+  | tInt _ | tFloat _ | tString _ => unit
   | tArray u arr def ty => All (wf Σ) arr * wf Σ def * wf Σ ty
   | tEvar n l => All (wf Σ) l
   | tCast t k t' => wf Σ t * wf Σ t'
@@ -152,10 +153,11 @@ Lemma term_wf_forall_list_ind Σ :
     (forall (m : mfixpoint term) (n : nat), tFixProp P P m -> P (tCoFix m n)) ->
     (forall i, P (tInt i)) ->
     (forall f, P (tFloat f)) ->
+    (forall s, P (tString s)) ->
     (forall u arr def ty, All P arr -> P def -> P ty ->  P (tArray u arr def ty)) ->
     forall t : term, wf Σ t -> P t.
 Proof.
-  intros P H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H17 H18 H19 Harr.
+  intros P H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H17 H18 H19 H20 Harr.
   intros until t. revert t.
   apply (term_forall_list_rect (fun t => wf Σ t -> P t));
     intros; try solve [match goal with
diff --git a/template-pcuic/theories/PCUICToTemplate.v b/template-pcuic/theories/PCUICToTemplate.v
index a1f4d1933..f97a7ffda 100644
--- a/template-pcuic/theories/PCUICToTemplate.v
+++ b/template-pcuic/theories/PCUICToTemplate.v
@@ -17,6 +17,7 @@ Definition trans_prim (trans : PCUICAst.term -> Ast.term) (t : prim_val) : Ast.t
   match t.π2 with
   | primIntModel i => Ast.tInt i
   | primFloatModel f => Ast.tFloat f
+  | primStringModel s => Ast.tString s
   | primArrayModel a => Ast.tArray (array_level a) (map trans (array_value a)) (trans (array_default a)) (trans (array_type a))
   end.
 
diff --git a/template-pcuic/theories/PCUICToTemplateCorrectness.v b/template-pcuic/theories/PCUICToTemplateCorrectness.v
index fcbbf40bd..cbcdb506f 100644
--- a/template-pcuic/theories/PCUICToTemplateCorrectness.v
+++ b/template-pcuic/theories/PCUICToTemplateCorrectness.v
@@ -2364,13 +2364,12 @@ Proof.
     + fold trans;subst types.
       now apply trans_mfix_All2.
     + now rewrite trans_wf_cofixpoint.
-  - cbn. destruct p as [? []]; simp prim_type; cbn; econstructor; eauto.
-    1,3,5: eapply trans_declared_constant; tea.
+  - destruct p as [? []]; simp prim_type; cbn; econstructor; eauto.
+    1,3,5,7: eapply trans_declared_constant; tea.
     all:cbn in *.
     all:move: H1; rewrite /Ast.Env.primitive_invariants /primitive_invariants.
-    1-2:intros []; split => //;
+    all: try by intros []; split => //;
     destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //.
-    intros []; split => //. rewrite H1 //. rewrite H2 //.
     all:depelim X1; eauto. intros _. solve_all.
   - eapply TT.type_Conv.
     + eassumption.
diff --git a/template-pcuic/theories/TemplateMonadToPCUIC.v b/template-pcuic/theories/TemplateMonadToPCUIC.v
index ecf5d6711..fedee03ed 100644
--- a/template-pcuic/theories/TemplateMonadToPCUIC.v
+++ b/template-pcuic/theories/TemplateMonadToPCUIC.v
@@ -163,6 +163,7 @@ Section with_tc.
              ret (tCoFix mfix' idx)
          | Ast.tInt n => ret (tPrim (primInt; primIntModel n))
          | Ast.tFloat n => ret (tPrim (primFloat; primFloatModel n))
+         | Ast.tString n => ret (tPrim (primString; primStringModel n))
          | Ast.tArray l v d ty =>
             v' <- monad_map@{t u t t} monad_trans' v ;;
             d' <- monad_trans' d ;;
diff --git a/template-pcuic/theories/TemplateToPCUIC.v b/template-pcuic/theories/TemplateToPCUIC.v
index 7df5f442f..f7ec265c8 100644
--- a/template-pcuic/theories/TemplateToPCUIC.v
+++ b/template-pcuic/theories/TemplateToPCUIC.v
@@ -103,6 +103,7 @@ Section Trans.
     tCoFix mfix' idx
   | Ast.tInt n => tPrim (primInt; primIntModel n)
   | Ast.tFloat n => tPrim (primFloat; primFloatModel n)
+  | Ast.tString n => tPrim (primString; primStringModel n)
   | Ast.tArray l v d ty => tPrim (primArray; primArrayModel
     {| array_level := l;
        array_value := List.map trans v;
diff --git a/template-pcuic/theories/TemplateToPCUICCorrectness.v b/template-pcuic/theories/TemplateToPCUICCorrectness.v
index 00c3e3bd9..8bd267daf 100644
--- a/template-pcuic/theories/TemplateToPCUICCorrectness.v
+++ b/template-pcuic/theories/TemplateToPCUICCorrectness.v
@@ -383,6 +383,7 @@ Proof.
   - f_equal; auto; solve_all.
   - f_equal; auto.
   - f_equal; auto.
+  - f_equal; auto.
   - cbn; do 4 f_equal; auto.
     rewrite /map_array_model. f_equal; eauto. cbn. solve_all.
 Qed.
@@ -443,6 +444,7 @@ Proof.
   - f_equal; auto; solve_list.
   - f_equal; auto.
   - f_equal; auto.
+  - f_equal; auto.
   - cbn; f_equal; auto. rewrite /map_array_model; cbn; do 3 f_equal; eauto.
     solve_all.
 Qed.
@@ -482,6 +484,7 @@ Proof.
   - rewrite /id /map_predicate /=. f_equal; solve_all.
   - f_equal; auto.
   - f_equal; auto.
+  - f_equal; auto.
   - cbn. rewrite /mapu_array_model; cbn; do 4 f_equal; auto; solve_all.
 Qed.
 
@@ -2489,6 +2492,14 @@ Proof.
       intros []; split => //;
       destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //.
     + constructor.
+  - cbn. replace (tConst prim_ty []) with (prim_type (primString; primStringModel p) prim_ty) by now simp prim_type.
+    econstructor; cbn; eauto.
+    + rewrite trans_env_retroknowledge //.
+    + now apply forall_decls_declared_constant.
+    + move: H1; rewrite /Ast.Env.primitive_invariants /primitive_invariants.
+      intros []; split => //;
+      destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //.
+    + constructor.
   - cbn. set (a := {| array_level := _ |}).
     replace (tApp (tConst prim_ty [u]) (trans (trans_global_env Σ.1) ty)) with (prim_type (primArray; primArrayModel a) prim_ty) by now simp prim_type.
     econstructor; cbn; eauto.
diff --git a/template-pcuic/theories/TemplateToPCUICExpanded.v b/template-pcuic/theories/TemplateToPCUICExpanded.v
index 1e5443085..402aff766 100644
--- a/template-pcuic/theories/TemplateToPCUICExpanded.v
+++ b/template-pcuic/theories/TemplateToPCUICExpanded.v
@@ -237,6 +237,7 @@ Proof with eauto using expanded.
     eapply expanded_tConstruct_app. eauto. cbn. unfold trans_local. now rewrite length_map context_assumptions_map. solve_all.
   - repeat constructor.
   - repeat constructor.
+  - repeat constructor.
   - wf_inv wf [[] ?]. repeat cbn; constructor. constructor; cbn; eauto. solve_all.
 Qed.
 
diff --git a/utils/theories/Show.v b/utils/theories/Show.v
index 9f3f38704..1c5d5dca5 100644
--- a/utils/theories/Show.v
+++ b/utils/theories/Show.v
@@ -1,4 +1,4 @@
-From Coq Require Import PArith Sint63 String Uint63 PrimFloat SpecFloat FloatOps.
+From Coq Require Import PArith Sint63 String Uint63 PrimFloat SpecFloat FloatOps PString.
 From MetaCoq.Utils Require Import bytestring MCString.
 
 Local Open Scope bs_scope.
@@ -56,9 +56,22 @@ Definition string_of_prim_int (i:Uint63.int) : string :=
 Definition string_of_float (f : PrimFloat.float) : string :=
   string_of_specfloat (FloatOps.Prim2SF f).
 
+Definition char63_to_string (c : PrimString.char63) : string :=
+  let b :=
+    match Byte.of_N (BinInt.Z.to_N (Uint63.to_Z c)) with
+    | None => Byte.x00
+    | Some b => b
+    end
+  in
+  String.String b String.EmptyString.
+
+Definition string_of_pstring (s : PrimString.string) : string :=
+  string_of_list char63_to_string (PString.to_list s).
+
 #[export] Instance show_uint : Show PrimInt63.int := string_of_prim_int.
 #[export] Instance show_sint : Show int_wrapper := { show x := string_of_Z (Sint63.to_Z (x.(int_wrap))) }.
 #[export] Instance show_specfloat : Show SpecFloat.spec_float := string_of_specfloat.
 #[export] Instance show_float : Show PrimFloat.float := string_of_float.
 #[export] Instance show_positive : Show positive := string_of_positive.
 #[export] Instance show_Z : Show Z := string_of_Z.
+#[export] Instance show_pstring : Show PrimString.string := string_of_pstring.