Skip to content

Commit e140d15

Browse files
committed
[TC] move time-is-active and coercion-unify in db.v
1 parent ed5026a commit e140d15

File tree

2 files changed

+5
-4
lines changed

2 files changed

+5
-4
lines changed

apps/tc/elpi/tc_aux.elpi

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,6 @@ namespace tc {
173173
section-var->decl L :-
174174
section-var->decl.aux {coq.env.section} L.
175175

176-
pred time-is-active i:(list string -> prop).
177176
:name "time-is-active"
178177
time-is-active _ :- coq.option.get ["Time", "TC", "Bench"] (coq.option.bool tt), !.
179178
time-is-active Opt :- tc.is-option-active Opt.
@@ -220,9 +219,6 @@ namespace tc {
220219
int ->
221220
term.
222221

223-
:index (5)
224-
pred coercion-unify i:term.
225-
226222
type coercion
227223
term ->
228224
list term ->

apps/tc/theories/db.v

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,5 +102,10 @@ Elpi Db tc.db lp:{{
102102

103103
% relates a projection to the its record
104104
pred proj->record i:constant, o:term.
105+
106+
:index (5)
107+
pred coercion-unify i:term.
108+
109+
pred time-is-active i:(list string -> prop).
105110
}
106111
}}.

0 commit comments

Comments
 (0)