- let conclude subst metasenv ugraph last_tl1' last_tl2' =
- let subst',metasenv,ugraph =
-(*DEBUGGING ONLY:
-prerr_endline
- ("OK " ^ 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,ugraph as res =
-*)
- fo_unif_subst test_equality_only subst' context
- metasenv (C.Appl l1) (C.Appl l2) ugraph
-(*DEBUGGING ONLY:
-in
-(prerr_endline
- (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
- " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
-res)
-*)
- in
- let grow1 =
- match last_tl1 with Cic.Meta _ -> true | _ -> false in
- let grow2 =
- match last_tl2 with Cic.Meta _ -> true | _ -> false in
- if not (grow1 || grow2) then
- (* no flexible terminals -> no pullback, but
- * we still unify them, in some cases it helps *)
- conclude subst metasenv ugraph last_tl1 last_tl2
- else
+ let grow1 =
+ match last_tl1 with Cic.Meta _ -> true | _ -> false in
+ let grow2 =
+ match last_tl2 with Cic.Meta _ -> true | _ -> false in
+ if not (grow1 || grow2) then
+ let _,last_tl1 =
+ inner_coerced ~skip_non_c:true (Cic.Appl l1) in
+ let _,last_tl2 =
+ inner_coerced ~skip_non_c:true (Cic.Appl l2) in
+ conclude subst metasenv ugraph last_tl1 last_tl2
+ else