(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
CoercGraph.is_a_coercion c1 &&
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
CoercGraph.is_a_coercion c1 &&
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
| Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
| Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
(match is_composite1, is_composite2 with
| false, false -> raise exn
| true, false ->
(match is_composite1, is_composite2 with
| false, false -> raise exn
| true, false ->