"with depth"^string_of_int depth));
debug_print (lazy (AutoCache.cache_print context cache));
if sort = T (* && tl <> []*) then
- aux flags tables maxm cache ((metasenv,subst,gl)::tl)
(debug_print
(lazy (" FAILURE(not in prop)"));
aux flags tables maxm cache ((metasenv,subst,gl)::tl))