cleanup

LPCIC · Oct 2, 2024 · a9d89b5 · a9d89b5
1 parent 5dc3c35
commit a9d89b5
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
@@ -102,11 +102,15 @@ Elpi Db tc.db lp:{{
 
     % relates a projection to the its record type fully applied to fresh
     % variables, eg, rules have the shape: (pi P1 ... PN\ proj->record {{p}} {{r P1 .. PN}})
+    % MANUALLY INSERTED by TC.AddRecordFields
     pred proj->record i:constant, o:term.
 
+    % tells if a term is a coercion
+    % MANUALLY INSERTED by Elpi Accumulate
     :index (5)
     pred coercion-unify i:term.
 
+    % Used to print bench infos
     pred time-is-active i:(list string -> prop).
   }
 }}.