diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index da0e4ceec..066f2f606 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -158,7 +158,7 @@ namespace tc {
 
   pred remove-clause i:string.
   remove-clause ClauseName :-
-    add-tc-db _ (replace ClauseName) dummy.
+    @local! => add-tc-db _ (replace ClauseName) dummy.
 
   % [section-var->decl.aux L R] auxiliary function for `section-var->decl`
   pred section-var->decl.aux i:list constant, o:list prop.
diff --git a/apps/tc/tests/test_coercion.v b/apps/tc/tests/test_coercion.v
index dd30bf809..d9adc53dc 100644
--- a/apps/tc/tests/test_coercion.v
+++ b/apps/tc/tests/test_coercion.v
@@ -67,3 +67,26 @@ Module Vehicle.
   Qed.
 
 End Vehicle.
+
+Module foo.
+  Class B (i : nat).
+
+  Section s.
+    (* Class with coercion depending on section parameters *)
+    Context (A : Type).
+    Class C (i : nat) : Set := {
+      f (x : A) :: B i
+    }.
+  End s.
+End foo.
+
+Module foo1.
+  Class B (i : nat).
+
+  Section s.
+    (* Class with coercion not depending on section parameters *)
+    Class C (i : nat) : Set := {
+      f :: B i
+    }.
+  End s.
+End foo1.
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index bcb8474dc..972260495 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -86,10 +86,11 @@ Elpi Accumulate lp:{{
       Class Bird := IsAnimal :> Animal.
     ```
     The instance IsAnimal of type Bird -> Animal, is compiled before the
-    predicate for Bird; hence, Bird is not recognize as a premise of IsAnimal.
+    predicate for Bird; hence, it is not possible to add the premise
+    tc-Bird for the IsAnimal instance...
     This problem is due to the order in which the registers for Instance and
     Class creation are run.
-    The solution is to do the following two jobs when a class C is created:
+    The solution is to do the following jobs when a class C is created:
       1: for every projection P of C, if P is a coercion, the wrongly 
         compiled instance is replaced with a `dummy` clause.
       2: the predicate for the class is created