diff --git a/apps/coercion/tests/coercion.t/test.v b/apps/coercion/tests/coercion.t/test.v
index 932605cb2..de11d41db 100644
--- a/apps/coercion/tests/coercion.t/test.v
+++ b/apps/coercion/tests/coercion.t/test.v
@@ -1,4 +1,5 @@
 From elpi.apps Require Import coercion.
+#[warning="-deprecated-from-Coq"]
 From Coq Require Import Bool.
 
 Elpi Accumulate coercion.db lp:{{
diff --git a/apps/coercion/tests/coercion_open.t/test.v b/apps/coercion/tests/coercion_open.t/test.v
index c4d533305..56dd6e8f9 100644
--- a/apps/coercion/tests/coercion_open.t/test.v
+++ b/apps/coercion/tests/coercion_open.t/test.v
@@ -1,4 +1,5 @@
 From elpi.apps Require Import coercion.
+#[warning="-deprecated-from-Coq"]
 From Coq Require Import Arith ssreflect.
 
 Ltac my_solver := trivial with arith.
diff --git a/apps/tc/tests/bigTest.v b/apps/tc/tests/bigTest.v
index 8368d44c0..f1c776b06 100644
--- a/apps/tc/tests/bigTest.v
+++ b/apps/tc/tests/bigTest.v
@@ -882,14 +882,23 @@ instances *)
 Section prod_setoid.
   Context `{Equiv A, Equiv B}.
   Elpi Accumulate TC.Solver lp:{{
-    shorten tc-Coq.Classes.RelationClasses.{tc-Equivalence}.
+    /* uncomment when requiring Coq >= 8.21
+    shorten tc-Stdlib.Classes.RelationClasses.{tc-Equivalence}. */
+    /* remove below definition when requiring Coq >= 8.21 */
     :after "lastHook"
-    tc-Equivalence A RA R :-
+    tc-Coq.Classes.RelationClasses.tc-Equivalence A RA R :-
       RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
       RA' = {{@prod_relation _ _ _ _}},
       coq.unify-eq RA RA' ok,
       % coq.say A RA,
-      tc-Equivalence A RA' R.
+      tc-Coq.Classes.RelationClasses.tc-Equivalence A RA' R.
+    :after "lastHook"
+    tc-Stdlib.Classes.RelationClasses.tc-Equivalence A RA R :-
+      RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
+      RA' = {{@prod_relation _ _ _ _}},
+      coq.unify-eq RA RA' ok,
+      % coq.say A RA,
+      tc-Stdlib.Classes.RelationClasses.tc-Equivalence A RA' R.
   }}.
   (* Elpi Typecheck TC.Solver. *)