- (match xxx with
- | [] -> ()
- | (m2,_,c2,c2')::_ ->
- let m1,_,c1,c1' = carr,metasenv,to1,to2 in
- let unopt =
- function Some (_,t) -> CicPp.ppterm t
- | None -> "id"
- in
- HLog.warn
- ("There are two minimal joins of "^
- CoercDb.string_of_carr car1^" and "^
- CoercDb.string_of_carr car2^": " ^
- CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^
- unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^
- unopt c2^" + "^unopt c2'));
- let last_tl1',(subst,metasenv,ugraph) =
- match last_tl1,to1 with
- | Cic.Meta (i1,l1),Some (last,coerced) ->
- last,
+ warn_if_not_unique xxx to1 to2 carr car1 car2;
+ let last_tl1',(subst,metasenv,ugraph) =
+ match grow1,to1 with
+ | true,Some (last,coerced) ->
+ last,