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
let ty',ugraph1 = type_of_aux ~logger context s ugraph in
let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
let b,ugraph1 =
- R.are_convertible ~subst ~metasenv context ty ty' ugraph1
+ R.are_convertible ~subst ~metasenv context ty' ty ugraph1
in
if not b then
raise