fo_unif_l
test_equality_only subst metasenv (lr1, lr2) ugraph
with
- | UnificationFailure _
- | Uncertain _ as exn ->
+ | UnificationFailure s
+ | Uncertain s as exn ->
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
CoercGraph.is_a_coercion c1 &&
- CoercGraph.is_a_coercion c2 ->
+ CoercGraph.is_a_coercion c2 &&
+ not (UriManager.eq uri1 uri2) ->
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
| Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
| _ -> assert false
in
let is_composite1 =
- List.exists ((=) (`Class `Coercion)) attrs1 in
+ List.exists
+ (function `Class (`Coercion _) -> true | _-> false)
+ attrs1
+ in
let is_composite2 =
- List.exists ((=) (`Class `Coercion)) attrs2 in
+ List.exists
+ (function `Class (`Coercion _) -> true | _-> false)
+ attrs2
+ in
(match is_composite1, is_composite2 with
| false, false -> raise exn
| true, false ->