comment

hb.elpi

@@ -814,7 +814,7 @@ prod-src-is-factory Ty :- whd1 Ty Ty1, !, prod-src-is-factory Ty1.
 
 pred ty-deps i:term, o:list-w-params mixinname.
 ty-deps Ty ML :- ty-deps.aux Ty ML, !.
-ty-deps (prod N T _) (w-params.nil N T _\[]) :- T = {{Type}}, !.
+ty-deps (prod N T _) (w-params.nil N T _\[]) :- T = {{Type}}, !. % TODO: relax to any type later on.
 ty-deps T _ :- % TODO: forall p1 ... pn (T : indexed Type) with indexed being the id function
   coq.error "ty-deps: BUG: could not get the parameters and the dependencies of"
     {coq.term->string T}.