-prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1)) ;
-prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2)) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t1) <> tty then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1)) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t2) <> tty then prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2)) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t1) <> (CicTypeChecker.type_of_aux' metasenv' context' t2)
- then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1)) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2)) ;
-prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term));
+prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ;
+prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
+if (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <> tty then
+prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ;
+if (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u)) <> tty then
+prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
+if (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <>
+(fst (CicTypeChecker.type_of_aux' metasenv' context' t2 u))
+ then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ;
+prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' term u)));