cleanup

Author: gares

apps/tc/theories/db.v

@@ -100,7 +100,8 @@ Elpi Db tc.db lp:{{
 
     pred ho-link o:term, i:term, o:A.
 
-    % relates a projection to the its record
+    % 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}})
     pred proj->record i:constant, o:term.
 
     :index (5)