- 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