[TC] dummy clauses are local to sections

This aims to solve the compilation error produced by the compilation of

```
Module foo.
  Class B (i : nat).

  Section s.
    (* Class with coercion depending on section parameters *)
    Context (A : Type).
    Class C (i : A) : Set := {
      x (x : A) :: B 3
    }.
  End s.
End foo.
```

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.

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.

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