From a9d89b544cdb2cb4fd0dc9804b4addb8e5f11f87 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:16:47 +0200
Subject: [PATCH] cleanup

---
 apps/tc/theories/db.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 94497ced2..ca3c94dba 100644
--- 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).
   }
 }}.