let module R = CicReduction in
let module S = CicSubstitution in
let module U = UriManager in
+(* FG: DEBUG ONLY
+ prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context);
+ prerr_endline ("TC: term :\n" ^ CicPp.ppterm ~metasenv t ^ "\n");
+*)
match t with
C.Rel n ->
(try