[TC] move time-is-active and coercion-unify in db.v

LPCIC · Sep 30, 2024 · 25de1d1 · 25de1d1
1 parent ede3b19
commit 25de1d1
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
@@ -174,7 +174,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. 
@@ -221,9 +220,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
@@ -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).
   }
 }}.