diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index c34fb987a..3a36794d0 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -173,7 +173,6 @@ namespace tc {
   section-var->decl L :-
     section-var->decl.aux {coq.env.section} L.
 
-  pred time-is-active i:(list string -> prop).
   :name "time-is-active"
   time-is-active _ :- coq.option.get ["Time", "TC", "Bench"] (coq.option.bool tt), !.
   time-is-active Opt :- tc.is-option-active Opt. 
@@ -220,9 +219,6 @@ namespace tc {
     int ->
     term.
 
-  :index (5)
-  pred coercion-unify i:term.
-
   type coercion
     term ->
     list term ->
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 6fb9948b3..90618d9e2 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -102,5 +102,10 @@ Elpi Db tc.db lp:{{
 
     % relates a projection to the its record
     pred proj->record i:constant, o:term.
+    
+    :index (5)
+    pred coercion-unify i:term.
+
+    pred time-is-active i:(list string -> prop).
   }
 }}.