diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 3ab119660..ff2dd5fa7 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -98,6 +98,6 @@ jobs:
           GITHUB_DEBUG=1 opam-publish --no-confirmation --tag=$TAG \
             --packages-directory=${OPAM_SUITE:-released}/packages \
             --repo=rocq-prover/opam --no-browser -v ${TAG##v}	\
-            rocq-elpi.opam rocq-elpi-json.opam rocq-elpi-xml.opam \
+            rocq-elpi.opam rocq-elpi-json.opam rocq-elpi-xml.opam rocq-elpi-typeclasses.opam\
             coq-elpi.opam \
             https://github.com/LPCIC/coq-elpi/releases/download/$TAG/rocq-elpi-${TAG##v}.tar.gz
diff --git a/Changelog.md b/Changelog.md
index 684e4f4ad..0808dda62 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -21,6 +21,12 @@ Requires Elpi 3.7.1 and Rocq 9.0, 9.1 or 9.2.
 ### Plugins
 - New `xml` plugin containing minimal bindings to `xml-light`, see
   [apps/xml](apps/xml/) for the doc.
+- New `typeclasses` plugin containing rocq-elpi's typeclass solver, see
+  [apps/tc](apps/tc/) for the doc.
+
+### API
+- New `coq.TC.override-solver` builtin calling the
+  `Elpi TC Solver Override _ Add _` directive.
 
 ### API
 - Change `main-interp-proof` and `main-interp-qed` changed type to better chain
diff --git a/apps/tc/doc/dune b/apps/tc/doc/dune
new file mode 100644
index 000000000..5efc1871f
--- /dev/null
+++ b/apps/tc/doc/dune
@@ -0,0 +1,16 @@
+(executable
+ (name gen_doc)
+ (libraries elpi_tc_plugin))
+
+(rule
+ (targets
+  tc-builtin.elpi)
+ (deps gen_doc.exe)
+ (mode promote)
+ (action (run ./gen_doc.exe)))
+
+(install
+ (files
+  tc-builtin.elpi)
+ (section doc)
+ (package rocq-elpi-typeclasses))
diff --git a/apps/tc/doc/gen_doc.ml b/apps/tc/doc/gen_doc.ml
new file mode 100644
index 000000000..3130a43b4
--- /dev/null
+++ b/apps/tc/doc/gen_doc.ml
@@ -0,0 +1,3 @@
+
+let _ = Elpi.API.BuiltIn.document_file ~header:"% Generated"
+  Elpi_tc_plugin.Rocq_elpi_class_tactics_takeover.tc_builtins
diff --git a/apps/tc/src/dune b/apps/tc/src/dune
index 6c60a9c10..ebc96e820 100644
--- a/apps/tc/src/dune
+++ b/apps/tc/src/dune
@@ -1,6 +1,6 @@
 (library
  (name elpi_tc_plugin)
- (public_name rocq-elpi.tc)
+ (public_name rocq-elpi-typeclasses.elpi_tc_plugin)
  (flags :standard -w -27)
  (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
  (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi))
diff --git a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml
index 7a2c98085..2cea25d0b 100644
--- a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml
+++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml
@@ -180,6 +180,17 @@ let set_solver_mode kind qname (l: Libnames.qualid list) =
   | ANone-> Lib.add_leaf (cache_solver_mode (qname, Set (Only OSet.empty), false))
   | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only l), false))
 
+let tc_builtins = [
+  Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver",
+    In(Elpi.API.BuiltInData.string, "SolverName",
+    In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "ClassNames",
+    Easy("Declares that goals on classes in ClassNames should be solved using the typeclass solver SolverName."))),
+  (fun s gr ~depth ->
+    set_solver_mode AAdd [s] (List.map Libnames.qualid_of_string gr))), 
+  DocAbove)]
+
+let tc_builtins = API.BuiltIn.declare ~file_name:"tc-builtin.elpi" tc_builtins
+
 let solver_register l =
   Lib.add_leaf (Solver.cache_solver (l, Create));
   Lib.add_leaf (Modes.cache_solver_mode (l, Add OSet.empty, true))
diff --git a/apps/tc/src/rocq_elpi_class_tactics_takeover.mli b/apps/tc/src/rocq_elpi_class_tactics_takeover.mli
index 49ecce52c..062bf26e8 100644
--- a/apps/tc/src/rocq_elpi_class_tactics_takeover.mli
+++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.mli
@@ -8,3 +8,4 @@ val set_solver_mode : aaction -> string list -> Libnames.qualid list -> unit
 val solver_register : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit
 val solver_activate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit
 val solver_deactivate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit
+val tc_builtins : Elpi.API.Setup.builtins
diff --git a/apps/tc/src/rocq_elpi_tc_hook.mlg b/apps/tc/src/rocq_elpi_tc_hook.mlg
index 8c84d8855..9170c30fd 100644
--- a/apps/tc/src/rocq_elpi_tc_hook.mlg
+++ b/apps/tc/src/rocq_elpi_tc_hook.mlg
@@ -1,7 +1,7 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
-DECLARE PLUGIN "rocq-elpi.tc"
+DECLARE PLUGIN "rocq-elpi-typeclasses.elpi_tc_plugin"
 
 {
 open Stdarg
@@ -51,4 +51,4 @@ VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      set_solver_mode ARm (snd p) cs }
 
-END
\ No newline at end of file
+END
diff --git a/apps/tc/theories/dune b/apps/tc/theories/dune
index 6e7a83821..bcfd269b4 100644
--- a/apps/tc/theories/dune
+++ b/apps/tc/theories/dune
@@ -1,8 +1,8 @@
 (coq.theory
  (name elpi.apps.tc)
- (package rocq-elpi)
- (theories elpi elpi.apps.tc.elpi)
+ (package rocq-elpi-typeclasses)
+ (theories elpi_elpi elpi elpi.apps.tc.elpi)
  (flags -w -all -w -elpi)
- (plugins rocq-elpi.tc))
+ (plugins rocq-elpi.elpi rocq-elpi-typeclasses.elpi_tc_plugin))
 
 (include_subdirs qualified)
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 31cc2d4b9..510f2bd34 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -1,7 +1,8 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
-Declare ML Module "rocq-elpi.tc".
+From elpi Require Import elpi.
+Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin".
 
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 (* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *)
diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v
index d7060d727..f526c99fd 100644
--- a/apps/tc/theories/wip.v
+++ b/apps/tc/theories/wip.v
@@ -1,8 +1,9 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* --------------------------------------------------------------------------*)
 
-Declare ML Module "rocq-elpi.tc".
+(*
 From elpi Require Import elpi.
+Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin".
 
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
@@ -16,7 +17,7 @@ From elpi.apps.tc.elpi Extra Dependency "rewrite_forward.elpi" as rforward.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
-(* From elpi.apps Require Import tc.
+From elpi.apps Require Import tc.
 Set Warnings "+elpi".
 
 Elpi Command AddForwardRewriting.
diff --git a/dune-project b/dune-project
index a71a5bd67..e61b7179d 100644
--- a/dune-project
+++ b/dune-project
@@ -35,6 +35,12 @@
   ppx_optcomp
   (ocaml-lsp-server :with-dev-setup)))
 
+(package
+ (name rocq-elpi-typeclasses)
+ (synopsis "Typeclass solver in rocq-elpi")
+ (description "This package provides a typeclass solver written in Elpi, as well as the infrastructure for writing custom ones")
+ (depends rocq-elpi))
+
 (package
  (name rocq-elpi-json)
  (synopsis "Yojson bindings for rocq-elpi")
diff --git a/rocq-elpi-typeclasses.opam b/rocq-elpi-typeclasses.opam
new file mode 100644
index 000000000..61a6f9515
--- /dev/null
+++ b/rocq-elpi-typeclasses.opam
@@ -0,0 +1,29 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "TC bindings for rocq-elpi"
+description: "This package provides a typeclass solver written in Elpi, as well as the infrastructure for writing custom ones"
+maintainer: ["Enrico Tassi <enrico.tassi@inria.fr>"]
+authors: ["Enrico Tassi <enrico.tassi@inria.fr>"]
+license: "LGPL-2.1-or-later"
+homepage: "https://github.com/LPCIC/coq-elpi/apps/tc/"
+bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
+depends: [
+  "dune" {>= "3.13"}
+  "rocq-elpi"
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "etc/with-rocq-wrap.sh" {!coq-core:installed}
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/LPCIC/coq-elpi.git"