+ let conclude subst metasenv ugraph last_tl1' last_tl2' =
+ let subst',metasenv,ugraph =
+(*DEBUGGING ONLY:
+prerr_endline
+ ("conclude: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
+ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
+*)
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1' last_tl2' ugraph
+ in
+ if subst = subst' then raise exn
+ else
+(*DEBUGGING ONLY:
+let subst,metasenv,ugrph as res =
+*)
+ fo_unif_subst test_equality_only subst' context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph
+(*DEBUGGING ONLY:
+in
+(prerr_endline
+ ("OK: "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+ " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res)
+*)
+ in
+(*DEBUGGING ONLY:
+prerr_endline (Printf.sprintf
+"Pullback problem\nterm1: %s\nterm2: %s\ncar1: %s\ncar2: %s\nlast_tl1: %s
+last_tl2: %s\nhead1_c: %s\nhead2_c: %s\n"
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context)
+(CoercDb.string_of_carr car1)
+(CoercDb.string_of_carr car2)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1 context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2 context)
+(CoercDb.string_of_carr head1_c)
+(CoercDb.string_of_carr head2_c)
+);
+*)