- let (ey1, ty1) =
- let (_, ey ,ty) = CicUtil.lookup_meta goal1 metasenv in
- (ey, ty) in
- let (ey2, ty2) =
- let (_, ey ,ty) = CicUtil.lookup_meta goal2 metasenv in
- (ey, ty) in
+ let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
+ let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
+(*
+ prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
+*)