diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index af8131ba2..7fc88232f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -27,6 +27,10 @@ jobs:
         with:
           opam_file: 'rocq-elpi.opam'
           custom_image: ${{ matrix.image }}
+          after_script: |
+            sudo chmod -R a+w .
+            make all-examples
+            make all-tests
           export: 'OPAMWITHTEST OPAMIGNORECONSTRAINTS OPAMVERBOSE'  # space-separated list of variables
         env:
           OPAMWITHTEST: 'true'
diff --git a/Changelog.md b/Changelog.md
index 49747a356..a403dde1a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,10 @@
+# UNRELEASED
+
+### APPS:
+- derive: support for primitive strings in `param1` and `param1_trivial`
+- derive: support for `is_true` in `param1_trivial` (based on pre-existing
+  special support for `is_eq` and `is_bool`)
+
 # [2.5.0] 18/2/2025
 
 Requires Elpi 2.0.7 and Coq 8.20 or Rocq 9.0.
diff --git a/_CoqProject b/_CoqProject
index 1649816ab..af51a883d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,8 +8,8 @@
 
 # Theories
 
--Q theories elpi
--Q _build/default/theories elpi
+-R theories elpi
+-R _build/default/theories elpi
 -Q theories-stdlib elpi_stdlib
 -Q _build/default/theories-stdlib elpi_stdlib
 
diff --git a/apps/cs/tests/setup-project.sh b/apps/cs/tests/setup-project.sh
deleted file mode 120000
index c0d2a8f89..000000000
--- a/apps/cs/tests/setup-project.sh
+++ /dev/null
@@ -1 +0,0 @@
-../../../etc/setup-project.sh
\ No newline at end of file
diff --git a/apps/derive/elpi/eqType.elpi b/apps/derive/elpi/eqType.elpi
index 532586542..3714a12db 100644
--- a/apps/derive/elpi/eqType.elpi
+++ b/apps/derive/elpi/eqType.elpi
@@ -63,7 +63,6 @@ translate-record-constructor (field _ ID _ _) _ (error S) :- S is "unsupported r
 pred self o:eqb.trm.
 
 pred valid i:eqb.trm, o:diagnostic.
-valid (eqb.global X) ok :- global X = {{ PrimInt63.int }}, !.
 valid (eqb.global GR) ok :- eqType GR _, !.
 valid (eqb.app GR A Args) D :- eqType GR EQT, !, valid-eqType EQT [A|Args] D.
 valid T (error S) :- S is "not an eqType: " ^ {std.any->string T}.
@@ -86,7 +85,7 @@ irrelevant? (app [{{ @eq }}, global EqType, A, B]) (eqb.app EQ EQTYPE [A1,B1]) D
   term->trm A A1,
   term->trm B B1,
 ].
-irrelevant? T R D :- whd1 T T1, coq.say "whd" T T1, irrelevant? T1 R D.
+irrelevant? T R D :- whd1 T T1, irrelevant? T1 R D.
 
 pred term->trm i:term, o:eqb.trm, o:diagnostic.
 term->trm (global GR) (eqb.global GR) ok :- !.
diff --git a/apps/derive/tests/test_bcongr.v b/apps/derive/tests/test_bcongr.v
index 8d056cbd4..9babdd03f 100644
--- a/apps/derive/tests/test_bcongr.v
+++ b/apps/derive/tests/test_bcongr.v
@@ -29,6 +29,7 @@ Elpi derive.bcongr large.
 *)
 Elpi derive.bcongr prim_int.
 Elpi derive.bcongr prim_float.
+Elpi derive.bcongr prim_string.
 Elpi derive.bcongr fo_record.
 Elpi derive.bcongr pa_record.
 Elpi derive.bcongr pr_record.
diff --git a/apps/derive/tests/test_derive_corelib.v b/apps/derive/tests/test_derive_corelib.v
index 98c2406fc..13da08422 100644
--- a/apps/derive/tests/test_derive_corelib.v
+++ b/apps/derive/tests/test_derive_corelib.v
@@ -1,6 +1,6 @@
 (* Some standard data types using different features *)
-From elpi.core Require PrimInt63.
-From elpi.core Require PrimFloat.
+From elpi Require elpi.
+From elpi.core Require PrimInt63 PrimFloat PrimString.
 
 Module Coverage.
 
@@ -70,6 +70,7 @@ Inductive large :=
 
 Inductive prim_int := PI (i : PrimInt63.int).
 Inductive prim_float := PF (f : PrimFloat.float).
+Inductive prim_string := PS (s : lib:elpi.pstring).
 
 Record fo_record := { f1 : peano; f2 : unit; }.
 
@@ -91,6 +92,8 @@ Definition is_zero (n:peano) : bool :=
 
 Record sigma_bool := { depn : peano; depeq : is_zero depn = true }.
 
+Record sigma_bool2 := { depn2 : peano; depeq2 : lib:elpi.is_true (is_zero depn2) }.
+
 Fixpoint is_leq (n m:peano) : bool := 
   match n, m with 
   | Zero, _ => true 
diff --git a/apps/derive/tests/test_eq.v b/apps/derive/tests/test_eq.v
index 87737912a..1ff3dd1c5 100644
--- a/apps/derive/tests/test_eq.v
+++ b/apps/derive/tests/test_eq.v
@@ -23,6 +23,7 @@ Fail Elpi derive.eq iota.
 Elpi derive.eq large.
 Elpi derive.eq prim_int.
 Elpi derive.eq prim_float.
+Elpi derive.eq prim_string.
 Elpi derive.eq fo_record.
 Elpi derive.eq pa_record.
 Elpi derive.eq pr_record.
diff --git a/apps/derive/tests/test_eqK.v b/apps/derive/tests/test_eqK.v
index 90f0c25f0..edea470b7 100644
--- a/apps/derive/tests/test_eqK.v
+++ b/apps/derive/tests/test_eqK.v
@@ -37,6 +37,7 @@ Elpi derive.eqK large.
 *)
 Elpi derive.eqK prim_int.
 Elpi derive.eqK prim_float.
+Elpi derive.eqK prim_string.
 Elpi derive.eqK fo_record.
 Elpi derive.eqK pa_record.
 Elpi derive.eqK pr_record.
diff --git a/apps/derive/tests/test_eqOK.v b/apps/derive/tests/test_eqOK.v
index f07711e2e..61996f8ee 100644
--- a/apps/derive/tests/test_eqOK.v
+++ b/apps/derive/tests/test_eqOK.v
@@ -1,4 +1,4 @@
-From elpi.apps Require Import derive.eqOK.
+From elpi.apps Require Import derive.param1 derive.eqOK.
 
 From elpi.apps Require Import test_derive_corelib test_eqcorrect test_param1 test_param1_trivial.
 
@@ -31,6 +31,7 @@ Elpi derive.eqOK large.
 *)
 Elpi derive.eqOK prim_int.
 Fail Elpi derive.eqOK prim_float.
+Elpi derive.eqOK prim_string.
 Elpi derive.eqOK fo_record.
 Elpi derive.eqOK pa_record.
 Elpi derive.eqOK pr_record.
diff --git a/apps/derive/tests/test_eqType_ast.v b/apps/derive/tests/test_eqType_ast.v
index ae2c8d282..2d7d4d378 100644
--- a/apps/derive/tests/test_eqType_ast.v
+++ b/apps/derive/tests/test_eqType_ast.v
@@ -24,6 +24,7 @@ Fail Elpi derive.eqType.ast iota.
 Elpi derive.eqType.ast large.
 Elpi derive.eqType.ast prim_int.
 Fail Elpi derive.eqType.ast prim_float.
+Elpi derive.eqType.ast prim_string.
 Elpi derive.eqType.ast fo_record.
 Elpi derive.eqType.ast pa_record.
 Elpi derive.eqType.ast pr_record.
@@ -32,6 +33,7 @@ Elpi derive.eqType.ast enum.
 Elpi derive.eqType.ast bool.
 Fail Elpi derive.eqType.ast eq.
 Elpi derive.eqType.ast sigma_bool.
+Elpi derive.eqType.ast sigma_bool2.
 Elpi derive.eqType.ast ord.
 Elpi derive.eqType.ast ord2.
 Elpi derive.eqType.ast val.
diff --git a/apps/derive/tests/test_eqb.v b/apps/derive/tests/test_eqb.v
index 09095d2e5..48d7c7a19 100644
--- a/apps/derive/tests/test_eqb.v
+++ b/apps/derive/tests/test_eqb.v
@@ -26,6 +26,7 @@ Elpi derive.eqb large.
 *)
 Elpi derive.eqb prim_int.
 Fail Elpi derive.eqb prim_float.
+Elpi derive.eqb prim_string.
 Elpi derive.eqb fo_record.
 Elpi derive.eqb pa_record.
 Elpi derive.eqb pr_record.
@@ -34,6 +35,7 @@ Elpi derive.eqb enum.
 Fail Elpi derive.eqb eq.
 Elpi derive.eqb bool.
 Elpi derive.eqb sigma_bool.
+Elpi derive.eqb sigma_bool2.
 Elpi derive.eqb ord.
 Elpi derive.eqb ord2.
 Elpi derive.eqb val.
diff --git a/apps/derive/tests/test_eqbOK.v b/apps/derive/tests/test_eqbOK.v
index 1db6f062b..76e5022d4 100644
--- a/apps/derive/tests/test_eqbOK.v
+++ b/apps/derive/tests/test_eqbOK.v
@@ -32,6 +32,7 @@ Elpi derive.eqbOK large.
 *)
 Elpi derive.eqbOK prim_int.
 Fail Elpi derive.eqbOK prim_float.
+Elpi derive.eqbOK prim_string.
 Elpi derive.eqbOK fo_record.
 Elpi derive.eqbOK pa_record.
 Elpi derive.eqbOK pr_record.
@@ -40,6 +41,7 @@ Elpi derive.eqbOK enum.
 Fail Elpi derive.eqbOK eq.
 Elpi derive.eqbOK bool.
 Elpi derive.eqbOK sigma_bool.
+Elpi derive.eqbOK sigma_bool2.
 Elpi derive.eqbOK ord.
 Elpi derive.eqbOK ord2.
 Elpi derive.eqbOK val.
diff --git a/apps/derive/tests/test_eqbcorrect.v b/apps/derive/tests/test_eqbcorrect.v
index fabb3a5b8..e6e6e9516 100644
--- a/apps/derive/tests/test_eqbcorrect.v
+++ b/apps/derive/tests/test_eqbcorrect.v
@@ -37,6 +37,7 @@ Elpi derive.eqbcorrect large.
 *)
 Elpi derive.eqbcorrect prim_int.
 Fail Elpi derive.eqbcorrect prim_float. (* Can not work, we don't have a syntaxtic test *)
+Elpi derive.eqbcorrect prim_string.
 Elpi derive.eqbcorrect fo_record.
 Elpi derive.eqbcorrect pa_record.
 Elpi derive.eqbcorrect pr_record.   
@@ -45,6 +46,7 @@ Elpi derive.eqbcorrect enum.
 Fail Elpi derive.eqbcorrect eq.
 Elpi derive.eqbcorrect bool.
 Elpi derive.eqbcorrect sigma_bool.
+Elpi derive.eqbcorrect sigma_bool2.
 Elpi derive.eqbcorrect ord.
 Elpi derive.eqbcorrect ord2.
 Elpi derive.eqbcorrect val.
diff --git a/apps/derive/tests/test_eqcorrect.v b/apps/derive/tests/test_eqcorrect.v
index 195526058..c25f77545 100644
--- a/apps/derive/tests/test_eqcorrect.v
+++ b/apps/derive/tests/test_eqcorrect.v
@@ -32,6 +32,7 @@ Elpi derive.eqcorrect large.
 *)
 Elpi derive.eqcorrect prim_int.
 Fail Elpi derive.eqcorrect prim_float.
+Elpi derive.eqcorrect prim_string.
 Elpi derive.eqcorrect fo_record.
 Elpi derive.eqcorrect pa_record.
 Elpi derive.eqcorrect pr_record.
diff --git a/apps/derive/tests/test_fields.v b/apps/derive/tests/test_fields.v
index 1ce2e1c95..f6b7b2368 100644
--- a/apps/derive/tests/test_fields.v
+++ b/apps/derive/tests/test_fields.v
@@ -24,6 +24,7 @@ Fail Elpi derive.fields iota.
 Elpi derive.fields large.
 Elpi derive.fields prim_int.
 Fail Elpi derive.fields prim_float.
+Elpi derive.fields prim_string.
 Elpi derive.fields fo_record.
 Elpi derive.fields pa_record.
 Elpi derive.fields pr_record.
@@ -32,6 +33,7 @@ Elpi derive.fields enum.
 Elpi derive.fields bool.
 Fail Elpi derive.fields eq.
 Elpi derive.fields sigma_bool.
+Elpi derive.fields sigma_bool2.
 Elpi derive.fields ord.
 Elpi derive.fields ord2.
 Elpi derive.fields val.
diff --git a/apps/derive/tests/test_induction.v b/apps/derive/tests/test_induction.v
index 1f8f7716a..10bb2f54d 100644
--- a/apps/derive/tests/test_induction.v
+++ b/apps/derive/tests/test_induction.v
@@ -28,14 +28,15 @@ Elpi derive.induction iota.
 Elpi derive.induction large.
 Elpi derive.induction prim_int.
 Elpi derive.induction prim_float.
+Elpi derive.induction prim_string.
 Elpi derive.induction fo_record.
 Elpi derive.induction pa_record.
 Elpi derive.induction pr_record.
 Elpi derive.induction dep_record.
 Elpi derive.induction enum.
-Elpi derive.induction eq.
-Elpi derive.induction bool.
 Elpi derive.induction sigma_bool.
+Elpi derive.induction bool.
+Elpi derive.induction sigma_bool2.
 Elpi derive.induction ord.
 Elpi derive.induction ord2.
 Elpi derive.induction val.
@@ -66,5 +67,6 @@ Redirect "tmp" Check pr_record_induction : forall A pr P, (forall x, is_peano x
 Redirect "tmp" Check dep_record_induction : forall P, (forall x (px : is_peano x) y, is_vect unit is_unit x px y -> P (Build_dep_record x y)) -> forall x, is_dep_record x -> P x.
 Redirect "tmp" Check enum_induction : forall P, (P E1) -> (P E2) -> (P E3) -> forall x, is_enum x -> P x.
 Redirect "tmp" Check sigma_bool_induction.
+Redirect "tmp" Check sigma_bool2_induction.
 Redirect "tmp" Check ord_induction : forall p Pp P, (forall n Pn l, is_eq bool is_bool (is_leq n p) (is_is_leq n Pn p Pp) true is_true l -> P (mkOrd p n l)) -> forall (o : ord p), is_ord p Pp o -> P o.
 Redirect "tmp" Check ord2_induction : forall p Pp P, (forall (o1 : ord p), is_ord p Pp o1 -> forall (o2 : ord p), is_ord p Pp o2 -> P (mkOrd2 p o1 o2)) -> forall (o : ord2 p), is_ord2 p Pp o -> P o.
diff --git a/apps/derive/tests/test_isK.v b/apps/derive/tests/test_isK.v
index fa4c8519a..44b8cf474 100644
--- a/apps/derive/tests/test_isK.v
+++ b/apps/derive/tests/test_isK.v
@@ -24,6 +24,7 @@ Elpi derive.isK iota.
 Elpi derive.isK large.
 Elpi derive.isK prim_int.
 Elpi derive.isK prim_float.
+Elpi derive.isK prim_string.
 Elpi derive.isK fo_record.
 Elpi derive.isK pa_record.
 Elpi derive.isK pr_record.
diff --git a/apps/derive/tests/test_lens.v b/apps/derive/tests/test_lens.v
index f59cae3b5..bf2e887c6 100644
--- a/apps/derive/tests/test_lens.v
+++ b/apps/derive/tests/test_lens.v
@@ -24,7 +24,7 @@ intros; unfold _pf3.
 match goal with
 | |- x = {| over := fun f r => {| pf3 := f (_ r); pf4 := _ r |} ;
             view := _ |}
-    => idtac "ok"
+    => idtac
 | |- _ => fail "not primitive"
 end.
 Abort.
diff --git a/apps/derive/tests/test_map.v b/apps/derive/tests/test_map.v
index e056747f8..1e35b38c5 100644
--- a/apps/derive/tests/test_map.v
+++ b/apps/derive/tests/test_map.v
@@ -33,6 +33,7 @@ Elpi derive.map enum.
 Fail Elpi derive.map eq.
 Elpi derive.map bool.
 Elpi derive.map sigma_bool.
+Elpi derive.map sigma_bool2.
 Fail Elpi derive.map ord.
 Elpi derive.map val.
 End Coverage.
diff --git a/apps/derive/tests/test_param1.v b/apps/derive/tests/test_param1.v
index d38412db2..0b8d8867e 100644
--- a/apps/derive/tests/test_param1.v
+++ b/apps/derive/tests/test_param1.v
@@ -25,6 +25,7 @@ Elpi derive.param1 iota.
 Elpi derive.param1 large.
 Elpi derive.param1 prim_int.
 Elpi derive.param1 prim_float.
+Elpi derive.param1 prim_string.
 Elpi derive.param1 fo_record.
 Elpi derive.param1 pa_record.
 Elpi derive.param1 pr_record.
@@ -32,10 +33,11 @@ Elpi derive.param1 dep_record.
 Elpi derive.param1 enum.
 (*
 Elpi derive.param1 eq. (* done in param1.v *)
+Elpi derive.param1 bool. (* done in param1.v *)
 *)
-Elpi derive.param1 bool.
 Elpi derive.param1 is_zero.
 Elpi derive.param1 sigma_bool.
+Elpi derive.param1 sigma_bool2.
 Elpi derive.param1 is_leq.
 Elpi derive.param1 ord.
 Elpi derive.param1 ord2.
@@ -101,7 +103,6 @@ Fixpoint vec_length (A : Type) n (v : vec A n) :=
 Elpi derive.param1 vec_length.
 Elpi derive.param1 list.
 Elpi derive.param1 is_list.
-Elpi derive.param1 eq.
 
 Fixpoint plus' m n := match n with 0 => m | S n => S (plus' m n) end.
 Elpi derive.param1 plus'.
@@ -109,7 +110,6 @@ Elpi derive.param1 plus.
 Elpi derive.param1 prod.
 Elpi derive.param1 fst.
 Elpi derive.param1 snd.
-Elpi derive.param1 bool.
 Elpi derive.param1 Nat.divmod.
 Elpi derive.param1 Nat.div.
 
diff --git a/apps/derive/tests/test_param1_congr.v b/apps/derive/tests/test_param1_congr.v
index 61a02b6f6..c16a7bedb 100644
--- a/apps/derive/tests/test_param1_congr.v
+++ b/apps/derive/tests/test_param1_congr.v
@@ -29,6 +29,7 @@ Elpi derive.param1.congr is_large. (* slow *)
 *)
 Elpi derive.param1.congr is_prim_int.
 Elpi derive.param1.congr is_prim_float.
+Elpi derive.param1.congr is_prim_string.
 Elpi derive.param1.congr is_fo_record.
 Elpi derive.param1.congr is_pa_record.
 Elpi derive.param1.congr is_pr_record.
@@ -37,6 +38,7 @@ Elpi derive.param1.congr is_enum.
 Elpi derive.param1.congr is_bool.
 Elpi derive.param1.congr is_eq.
 Elpi derive.param1.congr is_sigma_bool.
+Elpi derive.param1.congr is_sigma_bool2.
 Elpi derive.param1.congr is_ord.
 Elpi derive.param1.congr is_val.
 End Coverage.
diff --git a/apps/derive/tests/test_param1_functor.v b/apps/derive/tests/test_param1_functor.v
index f41275e0d..404ed1ecb 100644
--- a/apps/derive/tests/test_param1_functor.v
+++ b/apps/derive/tests/test_param1_functor.v
@@ -1,4 +1,4 @@
-From elpi.apps Require Import derive.param1_functor.
+From elpi.apps Require Import derive.param1 derive.param1_functor.
 
 From elpi.apps.derive.tests Require Import test_derive_corelib test_param1.
 Import test_derive_corelib.Coverage.
@@ -26,14 +26,16 @@ Elpi derive.param1.functor is_iota.
 Elpi derive.param1.functor is_large.
 Elpi derive.param1.functor is_prim_int.
 Elpi derive.param1.functor is_prim_float.
+Elpi derive.param1.functor is_prim_string.
 Elpi derive.param1.functor is_fo_record.
 Elpi derive.param1.functor is_pa_record.
 Elpi derive.param1.functor is_pr_record.
 Elpi derive.param1.functor is_dep_record.
 Elpi derive.param1.functor is_enum.
-Fail Elpi derive.param1.functor param1.is_eq.
-Elpi derive.param1.functor is_bool.
+Fail Elpi derive.param1.functor derive.param1.exports.is_eq.
+Elpi derive.param1.functor derive.param1.exports.is_bool.
 Elpi derive.param1.functor is_sigma_bool.
+Elpi derive.param1.functor is_sigma_bool2.
 Elpi derive.param1.functor is_ord.
 Elpi derive.param1.functor is_ord2.
 Elpi derive.param1.functor is_val.
diff --git a/apps/derive/tests/test_param1_trivial.v b/apps/derive/tests/test_param1_trivial.v
index 76923ff86..5f301f574 100644
--- a/apps/derive/tests/test_param1_trivial.v
+++ b/apps/derive/tests/test_param1_trivial.v
@@ -28,6 +28,7 @@ Fail Elpi derive.param1.trivial is_iota.
 Elpi derive.param1.trivial is_large.
 Elpi derive.param1.trivial is_prim_int.
 Elpi derive.param1.trivial is_prim_float.
+Elpi derive.param1.trivial is_prim_string.
 Elpi derive.param1.trivial is_fo_record.
 Elpi derive.param1.trivial is_pa_record.
 Elpi derive.param1.trivial is_pr_record.
@@ -38,6 +39,7 @@ Elpi derive.param1.trivial is_bool.
 Elpi derive.param1.trivial is_eq. (* ad-hoc *)
 *)
 Elpi derive.param1.trivial is_sigma_bool.
+Elpi derive.param1.trivial is_sigma_bool2.
 Elpi derive.param1.trivial is_ord.
 Elpi derive.param1.trivial is_ord2.
 Elpi derive.param1.trivial is_val.
diff --git a/apps/derive/tests/test_projK.v b/apps/derive/tests/test_projK.v
index d49b9abf4..68b1beb6f 100644
--- a/apps/derive/tests/test_projK.v
+++ b/apps/derive/tests/test_projK.v
@@ -24,6 +24,7 @@ Elpi derive.projK iota.
 Elpi derive.projK large.
 Elpi derive.projK prim_int.
 Elpi derive.projK prim_float.
+Elpi derive.projK prim_string.
 Elpi derive.projK fo_record.
 Elpi derive.projK pa_record.
 Elpi derive.projK pr_record.
diff --git a/apps/derive/tests/test_tag.v b/apps/derive/tests/test_tag.v
index 4f9b1a6c0..4925e05b6 100644
--- a/apps/derive/tests/test_tag.v
+++ b/apps/derive/tests/test_tag.v
@@ -25,6 +25,7 @@ Elpi derive.tag iota.
 Elpi derive.tag large.
 Elpi derive.tag prim_int.
 Elpi derive.tag prim_float.
+Elpi derive.tag prim_string.
 Elpi derive.tag fo_record.
 Elpi derive.tag pa_record.
 Elpi derive.tag pr_record.
@@ -33,6 +34,7 @@ Elpi derive.tag enum.
 Elpi derive.tag eq.
 Elpi derive.tag bool.
 Elpi derive.tag sigma_bool.
+Elpi derive.tag sigma_bool2.
 Elpi derive.tag ord.
 Elpi derive.tag ord2.
 Elpi derive.tag val.
diff --git a/apps/derive/theories/derive/eq.v b/apps/derive/theories/derive/eq.v
index 8f3238034..0aec76cfc 100644
--- a/apps/derive/theories/derive/eq.v
+++ b/apps/derive/theories/derive/eq.v
@@ -9,7 +9,7 @@ From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 
-From elpi.core Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 
 Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
 Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64.
@@ -20,6 +20,7 @@ Elpi Db derive.eq.db lp:{{
 type eq-db term -> term -> term -> prop.
 eq-db {{ lib:num.int63.type }} {{ lib:num.int63.type }} {{ lib:elpi.derive.eq_unit63 }} :- !.
 eq-db {{ lib:num.float.type }} {{ lib:num.float.type }} {{ lib:elpi.derive.eq_float64 }} :- !.
+eq-db {{ lib:elpi.pstring }} {{ lib:elpi.pstring }} {{ lib:elpi.pstring_eqb }} :- !.
 
 % quick access
 type eq-for inductive -> constant -> prop.
diff --git a/apps/derive/theories/derive/eqType_ast.v b/apps/derive/theories/derive/eqType_ast.v
index aae59728d..544c45331 100644
--- a/apps/derive/theories/derive/eqType_ast.v
+++ b/apps/derive/theories/derive/eqType_ast.v
@@ -1,5 +1,5 @@
 From elpi Require Import elpi.
-From elpi.core Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 From elpi.apps Require Import derive.
 
 From elpi.apps.derive.elpi Extra Dependency "eqType.elpi" as eqType.
@@ -29,6 +29,8 @@ type eqb.axiom       eqb.eqType.
 type eqb.constructor constructor -> eqb.arguments -> eqb.constructor.
 
 pred eqType i:gref, o:eqb.eqType.
+eqType {{:gref PrimInt63.int }} eqb.axiom :- !.
+eqType {{:gref lib:elpi.pstring }} eqb.axiom :- !.
 
 }}.
 
diff --git a/apps/derive/theories/derive/eqb.v b/apps/derive/theories/derive/eqb.v
index efa1ce8c0..ea4b02dd4 100644
--- a/apps/derive/theories/derive/eqb.v
+++ b/apps/derive/theories/derive/eqb.v
@@ -31,6 +31,7 @@ Elpi Db derive.eqb.db lp:{{
   
   eqb-for {{ PrimFloat.float }} {{ PrimFloat.float }} {{ PrimFloat.eqb }}.
   eqb-for {{ PrimInt63.int }} {{ PrimInt63.int }} {{ PrimInt63.eqb }}.
+  eqb-for {{ lib:elpi.pstring }} {{ lib:elpi.pstring }} {{ lib:elpi.pstring_eqb }}.
 
   :name "eqb-for:whd"
   eqb-for T1 T2 X :- whd1 T1 T1', !, eqb-for T1' T2 X. 
diff --git a/apps/derive/theories/derive/eqbcorrect.v b/apps/derive/theories/derive/eqbcorrect.v
index cea2a188a..91fb7d9ac 100644
--- a/apps/derive/theories/derive/eqbcorrect.v
+++ b/apps/derive/theories/derive/eqbcorrect.v
@@ -43,6 +43,19 @@ Proof. exact: Uint63Axioms.eqb_correct. Qed.
 Lemma uint63_eqb_refl i : eqb_refl_on PrimInt63.eqb i.
 Proof. exact: Uint63Axioms.eqb_refl. Qed.
 
+From elpi.core Require PrimString PrimStringAxioms.
+
+Lemma pstring_eqb_correct i : eqb_correct_on PrimString.eqb i.
+Proof.
+   move=> j; rewrite /PrimString.eqb; have [] := PrimStringAxioms.compare_ok i j.
+   by case: PrimString.compare => // /(_ erefl).
+Qed.
+
+Lemma pstring_eqb_refl i : eqb_refl_on PrimString.eqb i.
+Proof.
+   rewrite /PrimString.eqb /eqb_refl_on; have [] := PrimStringAxioms.compare_ok i i.
+   by case: PrimString.compare => // _ /(_ erefl).
+Qed.
 
 Elpi Db derive.eqbcorrect.db lp:{{
 
@@ -58,10 +71,12 @@ Elpi Db derive.eqbcorrect.db lp:{{
   :index(2)
   pred correct-lemma-for i:term, o:term.
   correct-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_correct }}.
+  correct-lemma-for {{ PrimString.string }} {{ @pstring_eqb_correct }}.
 
   :index(2)
   pred refl-lemma-for i:term, o:term.
   refl-lemma-for {{ PrimInt63.int }} {{ @uint63_eqb_refl }}.
+  refl-lemma-for {{ PrimString.string }} {{ @pstring_eqb_refl }}.
 
 }}.
 
diff --git a/apps/derive/theories/derive/eqcorrect.v b/apps/derive/theories/derive/eqcorrect.v
index 3c0353849..210bee200 100644
--- a/apps/derive/theories/derive/eqcorrect.v
+++ b/apps/derive/theories/derive/eqcorrect.v
@@ -11,25 +11,39 @@ From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 From elpi.apps Require Import  derive.eq derive.induction derive.eqK derive.param1.
 
-From elpi.core Require Import ssreflect PrimInt63.
-From elpi.core Require Uint63Axioms.
+From elpi.core Require Import ssreflect.
+
+From elpi.core Require PrimInt63 Uint63Axioms.
 
 Lemma uint63_eq_correct i : is_uint63 i -> eq_axiom_at PrimInt63.int PrimInt63.eqb i.
 Proof.
-move=> _ j; have [] : (eqb i j) = true <-> i = j.
+move=> _ j; have [] : (PrimInt63.eqb i j) = true <-> i = j.
   split; first exact: Uint63Axioms.eqb_correct.
   by move=> ->; rewrite Uint63Axioms.eqb_refl.
 by case: PrimInt63.eqb => [-> // _| _ abs]; constructor=> // /abs.
 Qed.
 Register uint63_eq_correct as elpi.derive.uint63_eq_correct.
 
+From elpi.core Require PrimString PrimStringAxioms.
+
+Lemma pstring_eq_correct i : is_pstring i -> eq_axiom_at PrimString.string PrimString.eqb i.
+Proof.
+  move=> _ j; have [] : (PrimString.eqb i j) = true <-> i = j.
+  rewrite /PrimString.eqb; have := PrimStringAxioms.compare_ok i j.
+   case: PrimString.compare => - [c r] //; split => //; [move=> _| by move=>/r ..].
+   by apply: c.
+by case: PrimString.eqb => [-> // _| _ abs]; constructor=> // /abs.
+Qed.
+Register pstring_eq_correct as elpi.derive.pstring_eq_correct.
+
 Elpi Db derive.eqcorrect.db lp:{{
   type eqcorrect-db gref -> term -> prop.
 }}.
 #[superglobal] Elpi Accumulate derive.eqcorrect.db File derive.lib.
 #[superglobal] Elpi Accumulate derive.eqcorrect.db lp:{{
   
-eqcorrect-db X {{ lib:elpi.derive.uint63_eq_correct }} :- {{ lib:num.int63.type }} = global X, !.
+eqcorrect-db {{:gref lib:num.int63.type }} {{ lib:elpi.derive.uint63_eq_correct }} :- !.
+eqcorrect-db {{:gref lib:elpi.pstring }} {{ lib:elpi.derive.pstring_eq_correct }} :- !.
 eqcorrect-db X _ :- {{ lib:num.float.type }} = global X, !, stop "float64 comparison is not syntactic".
 
 :name "eqcorrect-db:fail"
diff --git a/apps/derive/theories/derive/param1.v b/apps/derive/theories/derive/param1.v
index 5536da7c3..b3ec811ef 100644
--- a/apps/derive/theories/derive/param1.v
+++ b/apps/derive/theories/derive/param1.v
@@ -41,7 +41,7 @@ Class reali {X : Type} {XR : X -> Type} (x : X) (xR : XR x) := Reali {}.
 
 Register store_reali as param1.store_reali.
 
-From elpi.core Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 
 Inductive is_uint63 : PrimInt63.int -> Type := uint63 (i : PrimInt63.int) : is_uint63 i.
 Register is_uint63 as elpi.derive.is_uint63.
@@ -49,6 +49,9 @@ Register is_uint63 as elpi.derive.is_uint63.
 Inductive is_float64 : PrimFloat.float -> Type := float64 (f : PrimFloat.float ) : is_float64 f.
 Register is_float64 as elpi.derive.is_float64.
 
+Inductive is_pstring : PrimString.string -> Type := pstring (s : PrimString.string) : is_pstring s.
+Register is_pstring as elpi.derive.is_pstring.
+
 (* Links a term (constant, inductive type, inductive constructor) with
    its parametricity translation *)
 Elpi Db derive.param1.db lp:{{
@@ -62,6 +65,7 @@ pred reali-done i:gref.
 
 reali {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
 reali {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
+reali {{ lib:elpi.pstring }} {{ lib:elpi.derive.is_pstring }} :- !.
 
 :name "reali:fail"
 reali X _ :-
@@ -71,6 +75,7 @@ reali X _ :-
 
 realiR {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
 realiR {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
+realiR {{ lib:elpi.pstring }} {{ lib:elpi.derive.is_pstring }} :- !.
 
 :name "realiR:fail"
 realiR T TR :-
@@ -93,10 +98,20 @@ Elpi Accumulate lp:{{
 }}. 
 
 Module Export exports.
+
+Local Notation core_is_true := is_true. (* avoid shadowing by param1 is_true *)
+
 Elpi derive.param1 eq.
+Elpi derive.param1 bool.
+Elpi derive.param1 core_is_true.
+
 End exports.
-Register is_eq as elpi.derive.is_eq.
 
+Register is_eq as elpi.derive.is_eq.
+Register is_bool as elpi.derive.is_bool.
+Register is_true as elpi.derive.is_true.
+Register is_false as elpi.derive.is_false.
+Register is_is_true as elpi.derive.is_is_true.
 
 (* hook into derive *)
 Elpi Accumulate derive File paramX.
diff --git a/apps/derive/theories/derive/param1_trivial.v b/apps/derive/theories/derive/param1_trivial.v
index 858043cbc..d1099c9ad 100644
--- a/apps/derive/theories/derive/param1_trivial.v
+++ b/apps/derive/theories/derive/param1_trivial.v
@@ -16,58 +16,7 @@ From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.param1 derive.param1_congr.
 
-  
-Definition is_uint63_inhab x : is_uint63 x. Proof. constructor. Defined.
-Register is_uint63_inhab as elpi.derive.is_uint63_inhab.
-
-Definition is_float64_inhab x : is_float64 x. Proof. constructor. Defined.
-Register is_float64_inhab as elpi.derive.is_float64_inhab.
-
-Definition is_eq_inhab
-  A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x) y (py : PA y) (eq_xy : x = y) :
-    is_eq A PA x px y py eq_xy.
-Proof.
-  revert py.
-  case eq_xy; clear eq_xy y.
-  intro py.
-  rewrite <- (trivial_uniq A PA HA x px); clear px.
-  rewrite <- (trivial_uniq A PA HA x py); clear py.
-  apply (is_eq_refl A PA x (trivial_full A PA HA x)).
-Defined.
-Register is_eq_inhab as elpi.derive.is_eq_inhab.
-
-Definition is_uint63_trivial : trivial PrimInt63.int is_uint63 :=
-  fun x => contracts _ is_uint63 x (is_uint63_inhab x)
-    (fun y => match y with uint63 i => eq_refl end).
-Register is_uint63_trivial as elpi.derive.is_uint63_trivial.
-  
-Definition is_float64_trivial : trivial PrimFloat.float is_float64 :=
-  fun x => contracts _ is_float64 x (is_float64_inhab x)
-    (fun y => match y with float64 i => eq_refl end).
-Register is_float64_trivial as elpi.derive.is_float64_trivial.
-
-Lemma is_eq_trivial A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x) 
-   y (py : PA y)
-  : trivial (x = y) (is_eq A PA x px y py).
-Proof.
-  intro p.
-  apply (contracts (x = y) (is_eq A PA x px y py) p (is_eq_inhab A PA HA x px y py p)).
-  revert py.
-  case p; clear p y.
-  rewrite <- (trivial_uniq _ _ HA x px). clear px.
-  intros py.
-  rewrite <- (trivial_uniq _ _ HA x py). clear py.
-  intro v; case v; clear v.
-  unfold is_eq_inhab.
-  unfold trivial_full.
-  unfold trivial_uniq.
-  case (HA x); intros it def_it; compute.
-  case (def_it it).
-  reflexivity.
-Defined.
-Register is_eq_trivial as elpi.derive.is_eq_trivial.
-
-Elpi Db derive.param1.trivial.db lp:{{
+  Elpi Db derive.param1.trivial.db lp:{{
 
   pred param1-trivial-done i:inductive.
   type param1-trivial-db term -> term -> prop.
@@ -82,13 +31,7 @@ Elpi Db derive.param1.trivial.db lp:{{
 #[superglobal] Elpi Accumulate derive.param1.trivial.db Db Header derive.param1.db.
 #[superglobal] Elpi Accumulate derive.param1.trivial.db lp:{{
 
-  pred coq.mk-app i:term, i:list term, o:term.
-  pred coq.sort? i:term.
-
-  param1-inhab-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_inhab }}.
-  param1-inhab-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_inhab }}.
-  param1-inhab-db {{ lib:elpi.derive.is_eq }} {{ lib:elpi.derive.is_eq_inhab }}.
-
+  :name "param1:inhab:start"
   param1-inhab-db (fun `f` (prod `_` S _\ T) f\
               prod `x` S x\ prod `px` (RS x) _)
             (fun `f` (prod `_` S _\ T) f\
@@ -98,11 +41,6 @@ Elpi Db derive.param1.trivial.db lp:{{
               reali T R,
               param1-inhab-db R PT,
               coq.mk-app PT [{coq.mk-app f [x]}] (P f x).
-              
-  param1-inhab-db
-    {{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
-    {{ lib:elpi.derive.is_eq_inhab lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :- !,
-    param1-trivial-db PA QA.
 
   param1-inhab-db (app [Hd|Args]) (app[P|PArgs]) :-
     param1-inhab-db Hd P, !,
@@ -115,9 +53,7 @@ Elpi Db derive.param1.trivial.db lp:{{
        (param1-inhab-db P Q, R = [T,P,Q|PArgs], param1-inhab-db-args Args PArgs)
        (R = [T,P|PArgs], param1-inhab-db-args Args PArgs).
    
-  param1-trivial-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_trivial }}.
-  param1-trivial-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_trivial }}.
-
+  :name "param1:trivial:start"
   param1-trivial-db (fun `f` (prod `_` S _\ T) f\
               prod `x` S x\ prod `px` (RS x) _)
             (fun `f` (prod `_` S _\ T) f\
@@ -128,11 +64,6 @@ Elpi Db derive.param1.trivial.db lp:{{
               param1-trivial-db R PT,
               coq.mk-app PT [{coq.mk-app f [x]}] (P f x).
 
-  param1-trivial-db
-    {{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
-    {{ lib:elpi.derive.is_eq_trivial lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :-
-    param1-trivial-db PA QA.
-
   param1-trivial-db (app [Hd|Args]) (app[P|PArgs]) :-
     param1-trivial-db Hd P, !,
     param1-trivial-db-args Args PArgs.
@@ -146,6 +77,7 @@ Elpi Db derive.param1.trivial.db lp:{{
 
 }}.
   
+
 (* standalone *)
 Elpi Command derive.param1.trivial.
 Elpi Accumulate File derive_hook.
@@ -184,7 +116,132 @@ Elpi Accumulate lp:{{
     coq.error "Usage: derive.param1.inhab <inductive type name>".
 }}.
 
+(* ad-hoc rules for primitive data, eq and is_true *)
+
+Module Export exports.
+Elpi derive.param1.trivial is_bool.
+End exports.
+
+Definition is_uint63_inhab x : is_uint63 x. Proof. constructor. Defined.
+Register is_uint63_inhab as elpi.derive.is_uint63_inhab.
+
+Definition is_float64_inhab x : is_float64 x. Proof. constructor. Defined.
+Register is_float64_inhab as elpi.derive.is_float64_inhab.
+
+Definition is_pstring_inhab s : is_pstring s. Proof. constructor. Defined.
+Register is_pstring_inhab as elpi.derive.is_pstring_inhab.
 
+Definition is_eq_inhab
+  A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x) y (py : PA y) (eq_xy : x = y) :
+    is_eq A PA x px y py eq_xy.
+Proof.
+  revert py.
+  case eq_xy; clear eq_xy y.
+  intro py.
+  rewrite <- (trivial_uniq A PA HA x px); clear px.
+  rewrite <- (trivial_uniq A PA HA x py); clear py.
+  apply (is_eq_refl A PA x (trivial_full A PA HA x)).
+Defined.
+Register is_eq_inhab as elpi.derive.is_eq_inhab.
+
+Definition is_true_inhab b (H : is_bool b) p : is_is_true b H p :=
+  is_eq_inhab bool is_bool is_bool_trivial b H true is_true p.
+Register is_true_inhab as elpi.derive.is_true_inhab.
+
+
+Elpi Accumulate derive.param1.trivial.db lp:{{
+
+  :before "param1:inhab:start"
+  param1-inhab-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_inhab }}.
+  :before "param1:inhab:start"
+  param1-inhab-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_inhab }}.
+  :before "param1:inhab:start"
+  param1-inhab-db {{ lib:elpi.derive.is_pstring }} {{ lib:elpi.derive.is_pstring_inhab }}.
+  :before "param1:inhab:start"
+  param1-inhab-db {{ lib:elpi.derive.is_eq }} {{ lib:elpi.derive.is_eq_inhab }}.
+  :before "param1:inhab:start"
+  param1-inhab-db {{ lib:elpi.derive.is_true }} {{ lib:elpi.derive.is_true_inhab }}.
+
+
+  :before "param1:inhab:start"
+  param1-inhab-db
+    {{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
+    {{ lib:elpi.derive.is_eq_inhab lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :- !,
+    param1-trivial-db PA QA.
+
+  :before "param1:inhab:start"
+  param1-inhab-db {{ lib:elpi.derive.is_is_true lp:B lp:PB }} R :- !,
+    param1-inhab-db {{ lib:elpi.derive.is_eq lib:elpi.bool lib:elpi.derive.is_bool lp:B lp:PB lib:elpi.true lib:elpi.derive.is_true }} R.
+
+}}.
+
+
+Definition is_uint63_trivial : trivial PrimInt63.int is_uint63 :=
+  fun x => contracts _ is_uint63 x (is_uint63_inhab x)
+    (fun y => match y with uint63 i => eq_refl end).
+Register is_uint63_trivial as elpi.derive.is_uint63_trivial.
+  
+Definition is_float64_trivial : trivial PrimFloat.float is_float64 :=
+  fun x => contracts _ is_float64 x (is_float64_inhab x)
+    (fun y => match y with float64 i => eq_refl end).
+Register is_float64_trivial as elpi.derive.is_float64_trivial.
+
+Definition is_pstring_trivial : trivial lib:elpi.pstring is_pstring :=
+  fun x => contracts _ is_pstring x (is_pstring_inhab x)
+    (fun y => match y with pstring i => eq_refl end).
+Register is_pstring_trivial as elpi.derive.is_pstring_trivial.
+
+Lemma is_eq_trivial A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x) 
+   y (py : PA y)
+  : trivial (x = y) (is_eq A PA x px y py).
+Proof.
+  intro p.
+  apply (contracts (x = y) (is_eq A PA x px y py) p (is_eq_inhab A PA HA x px y py p)).
+  revert py.
+  case p; clear p y.
+  rewrite <- (trivial_uniq _ _ HA x px). clear px.
+  intros py.
+  rewrite <- (trivial_uniq _ _ HA x py). clear py.
+  intro v; case v; clear v.
+  unfold is_eq_inhab.
+  unfold trivial_full.
+  unfold trivial_uniq.
+  case (HA x); intros it def_it; compute.
+  case (def_it it).
+  reflexivity.
+Defined.
+Register is_eq_trivial as elpi.derive.is_eq_trivial.
+
+Definition is_true_trivial b (H : is_bool b) : trivial (lib:elpi.is_true b) (is_is_true b H) :=
+  is_eq_trivial bool is_bool is_bool_trivial b H true is_true.
+Register is_true_trivial as elpi.derive.is_true_trivial.
+
+
+Elpi Accumulate derive.param1.trivial.db lp:{{
+
+  :before "param1:trivial:start"
+  param1-trivial-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_trivial }}.
+  :before "param1:trivial:start"
+  param1-trivial-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_trivial }}.
+  :before "param1:trivial:start"
+  param1-trivial-db {{ lib:elpi.derive.is_pstring }} {{ lib:elpi.derive.is_pstring_trivial }}.
+  :before "param1:trivial:start"
+  param1-trivial-db {{ lib:elpi.derive.is_eq }} {{ lib:elpi.derive.is_eq_trivial }}.
+  :before "param1:trivial:start"
+  param1-trivial-db {{ lib:elpi.derive.is_true }} {{ lib:elpi.derive.is_true_trivial }}.
+
+
+  :before "param1:trivial:start"
+  param1-trivial-db
+    {{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
+    {{ lib:elpi.derive.is_eq_trivial lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :-
+    param1-trivial-db PA QA.
+
+  :before "param1:trivial:start"
+  param1-trivial-db {{ lib:elpi.derive.is_is_true lp:B lp:PB }} R :- !,
+    param1-trivial-db {{ lib:elpi.derive.is_eq lib:elpi.bool lib:elpi.derive.is_bool lp:B lp:PB lib:elpi.true lib:elpi.derive.is_true }} R.
+
+}}.
 
 (* hook into derive *)
 Elpi Accumulate derive Db derive.param1.trivial.db.
diff --git a/tests/test_elaborator.v b/tests/test_elaborator.v
index 7443f8403..19fb05199 100644
--- a/tests/test_elaborator.v
+++ b/tests/test_elaborator.v
@@ -1,4 +1,4 @@
-From elpi.core Require Import PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat PrimString.
 
 From elpi_elpi Extra Dependency "elpi_elaborator.elpi" as elab.
 
diff --git a/theories/core/PrimString.v.in b/theories/core/PrimString.v.in
new file mode 100644
index 000000000..2f71b941a
--- /dev/null
+++ b/theories/core/PrimString.v.in
@@ -0,0 +1,9 @@
+#[only="8.20"] From Coq Require PrimString.
+#[skip="8.20"] From Corelib Require PrimString.
+
+Register PrimString.string as elpi.pstring.
+
+Definition eqb (s1 s2 : PrimString.string) :=
+  match PrimString.compare s1 s2 with Eq => true | _ => false end.
+
+Register eqb as elpi.pstring_eqb.
diff --git a/theories/core/PrimStringAxioms.v.in b/theories/core/PrimStringAxioms.v.in
new file mode 100644
index 000000000..ac3fbc24e
--- /dev/null
+++ b/theories/core/PrimStringAxioms.v.in
@@ -0,0 +1,34 @@
+#[only="8.20"] From Coq Require Export PrimStringAxioms PString.
+#[only="8.20"] Definition compare_ok := compare_eq.
+
+#[skip="8.20"] From Corelib Require Import ssreflect ssrbool Uint63Axioms PrimStringAxioms.
+#[skip="8.20"] Lemma compare_refl (s : string) : compare s s = Eq.
+#[skip="8.20"] Proof.
+#[skip="8.20"]   rewrite PrimStringAxioms.compare_spec.
+#[skip="8.20"]   elim: (to_list s) => //= x xs ->.
+#[skip="8.20"]   rewrite Uint63Axioms.compare_def_spec /compare_def eqb_refl.
+#[skip="8.20"]   suff: ltb x x = false by move->.
+#[skip="8.20"]   have [+ _] := ltb_spec x x.
+#[skip="8.20"]   by case: ltb => // /(_ isT); case: (to_Z x) => //=; elim.
+#[skip="8.20"] Qed.
+#[skip="8.20"] Lemma to_list_inj (s1 s2 : string) :
+#[skip="8.20"]   to_list s1 = to_list s2 -> s1 = s2.
+#[skip="8.20"] Proof.
+#[skip="8.20"]   intros H. rewrite -(of_to_list s1) -(of_to_list s2) H.
+#[skip="8.20"]   reflexivity.
+#[skip="8.20"] Qed.
+#[skip="8.20"] Lemma compare_eq_correct (s1 s2 : string) :
+#[skip="8.20"]   compare s1 s2 = Eq -> s1 = s2.
+#[skip="8.20"] Proof.
+#[skip="8.20"]   move=> E; rewrite -[s1]of_to_list -[s2]of_to_list; congr (of_list _).
+#[skip="8.20"]   move: E; rewrite compare_spec.
+#[skip="8.20"]   elim: (to_list s1) (to_list s2) => [[]//|x xs IH [|y ys] //=].
+#[skip="8.20"]   rewrite Uint63Axioms.compare_def_spec /compare_def.
+#[skip="8.20"]   move: (eqb_correct x y); case: eqb => [/(_ isT)->|_].
+#[skip="8.20"]     suff: ltb y y = false by move=> -> /IH ->.
+#[skip="8.20"]     have [+ _] := ltb_spec y y.
+#[skip="8.20"]     by case: ltb => // /(_ isT); case: (to_Z y) => //=; elim.
+#[skip="8.20"]   by case: ltb.
+#[skip="8.20"] Qed.
+#[skip="8.20"] Lemma compare_ok (s1 s2 : string) : compare s1 s2 = Eq <-> s1 = s2.
+#[skip="8.20"] Proof. split; [apply compare_eq_correct|intros []; apply compare_refl]. Qed.
diff --git a/theories/core/dune b/theories/core/dune
index 2f8ad19b4..30d1808b8 100644
--- a/theories/core/dune
+++ b/theories/core/dune
@@ -49,6 +49,14 @@
   (with-stdout-to %{target}
    (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
 
+(rule
+ (target PrimString.v)
+ (deps
+  (glob_files PrimString.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
 (rule
  (target RelationClasses.v)
  (deps
@@ -73,6 +81,14 @@
   (with-stdout-to %{target}
    (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
 
+(rule
+ (target PrimStringAxioms.v)
+ (deps
+  (glob_files PrimStringAxioms.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
 (rule
  (target ssreflect.v)
  (deps
diff --git a/theories/elpi.v.in b/theories/elpi.v.in
index ece31feff..06180e1f1 100644
--- a/theories/elpi.v.in
+++ b/theories/elpi.v.in
@@ -46,12 +46,8 @@ Register Coq.Init.Datatypes.false as elpi.false.
 #[only="8.20"] Register Coq.Bool.Bool.reflect  as elpi.reflect.
 #[only="8.20"] Register Coq.Bool.Bool.ReflectF as elpi.ReflectF.
 #[only="8.20"] Register Coq.Bool.Bool.ReflectT as elpi.ReflectT.
+#[only="8.20"] Register Coq.Init.Datatypes.is_true as elpi.is_true.
 #[skip="8.20"] Register Corelib.Init.Datatypes.reflect  as elpi.reflect.
 #[skip="8.20"] Register Corelib.Init.Datatypes.ReflectF as elpi.ReflectF.
 #[skip="8.20"] Register Corelib.Init.Datatypes.ReflectT as elpi.ReflectT.
-
-#[only="8.20"] From Coq Require PrimString.
-#[skip="8.20"] From Corelib Require PrimString.
-
-#[only="8.20"] Register Coq.Strings.PrimString.string as elpi.pstring.
-#[skip="8.20"] Register Corelib.Strings.PrimString.string as elpi.pstring.
+#[skip="8.20"] Register Corelib.Init.Datatypes.is_true as elpi.is_true.