From ede3b19bf5c74da82a237ba3e0b154c8fc28b242 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 25 Sep 2024 16:12:59 +0200
Subject: [PATCH] [TC] add comment

---
 apps/tc/elpi/compile_goal.elpi | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 340c76f60..0abf16517 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -111,6 +111,9 @@ namespace tc {
       compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
     }
 
+    % [goal T T' L] takes a term T and returns a new term T' where problematic
+    % subterms (see this: https://dl.acm.org/doi/10.1145/3678232.3678233)
+    % are replaced with fresh variables. The list of links is L
     pred goal i:term, o:term, o:list prop.
     :name "compile-goal"
     goal Goal Goal' Links :-