[TC] premise w/solution add comment

apps/tc/elpi/tc_aux.elpi

@@ -109,6 +109,16 @@ pred get-mode i:gref, o:list string.
 get-mode ClassGR M :- class ClassGR _ _ M, !.
 get-mode ClassGR _ :- coq.error "[TC]" ClassGR "is an unknown class".
 
+/* 
+[make-tc.aux B Sol Head Body Rule] builds the rule with the given Head and body
+                                   paying attention to the positivity of the
+                                   clause  
+Note: if the Rule being constructed is negative (B = ff), then Rules returns a
+      solution Sol used inside the proof. If the solution is already given, we
+      do not run the premise. This would ask Sol to be ground (ground_term S).
+      Here, for performance issues, we simply check that the solution is not a
+      flexible term
+*/
 pred make-tc.aux i:bool, i:term, i:prop, i:list prop, o:prop.
 make-tc.aux tt _ Head [] Head :- !.
 make-tc.aux ff Sol Head [] P :- !, P = if (var Sol) Head true.