metasenv (C.Appl l1) (C.Appl l2) ugraph
| _ -> raise exn)
else
- let meets = CoercGraph.meets car1 car2 in
+ let meets =
+ CoercGraph.meets metasenv subst context car1 car2
+ in
(match meets with
| [] -> raise exn
- | _::_::_ ->
-prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-let m1::m2::_ = meets in
-prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2);
-assert false
- | [m] ->
+ | (carr,metasenv,to1,to2)::xxx ->
+ (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.name_of_carr car1^" and "^
+ CoercDb.name_of_carr car2^": " ^
+ CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
+ unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+ unopt c2^" + "^unopt c2'));
let last_tl1',(subst,metasenv,ugraph) =
- match last_tl1 with
- | Cic.Meta (i1,l1)
- when not (CoercDb.eq_carr m car1) ->
- (match
- CoercGraph.look_for_coercion' metasenv subst
- context m car1
- with
- | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
- ->
- last,
- fo_unif_subst test_equality_only subst context
+ match last_tl1,to1 with
+ | Cic.Meta (i1,l1),Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
metasenv coerced last_tl1 ugraph
- | _ ->
-prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
- | _ -> last_tl1,(subst,metasenv,ugraph) in
+ | _ -> last_tl1,(subst,metasenv,ugraph)
+ in
let last_tl2',(subst,metasenv,ugraph) =
- match last_tl2 with
- Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) ->
- (match
- CoercGraph.look_for_coercion' metasenv subst
- context m car2
- with
- (*CSC: bu here: I am considering only the first one*)
- | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
- ->
- last,
- fo_unif_subst test_equality_only subst context
+ match last_tl2,to2 with
+ | Cic.Meta (i2,l2),Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
metasenv coerced last_tl2 ugraph
- | _ ->
-prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
- | _ -> last_tl2,(subst,metasenv,ugraph)
+ | _ -> last_tl2,(subst,metasenv,ugraph)
in
-(*DEBUGGING ONLY:
+ (*DEBUGGING ONLY:
prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
*)
let subst,metasenv,ugraph =