+ test_equality_only subst metasenv (lr1, lr2) ugraph
+ with
+ | UnificationFailure _
+ | Uncertain _ 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 ->
+ let body1, attrs1, ugraph =
+ match CicEnvironment.get_obj ugraph uri1 with
+ | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
+ | _ -> assert false
+ in
+ let body2, attrs2, ugraph =
+ match CicEnvironment.get_obj ugraph uri2 with
+ | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
+ | _ -> assert false
+ in
+ let is_composite1 =
+ List.exists ((=) (`Class `Coercion)) attrs1 in
+ let is_composite2 =
+ List.exists ((=) (`Class `Coercion)) attrs2 in
+ (match is_composite1, is_composite2 with
+ | false, false -> raise exn
+ | true, false ->
+ let body1 = CicSubstitution.subst_vars ens1 body1 in
+ let appl = Cic.Appl (body1::tl1) in
+ let redappl = CicReduction.head_beta_reduce appl in
+ fo_unif_subst
+ test_equality_only subst context metasenv
+ redappl t2 ugraph
+ | false, true ->
+ let body2 = CicSubstitution.subst_vars ens2 body2 in
+ let appl = Cic.Appl (body2::tl2) in
+ let redappl = CicReduction.head_beta_reduce appl in
+ fo_unif_subst
+ test_equality_only subst context metasenv
+ t1 redappl ugraph
+ | true, true ->
+ let body1 = CicSubstitution.subst_vars ens1 body1 in
+ let appl1 = Cic.Appl (body1::tl1) in
+ let redappl1 = CicReduction.head_beta_reduce appl1 in
+ let body2 = CicSubstitution.subst_vars ens2 body2 in
+ let appl2 = Cic.Appl (body2::tl2) in
+ let redappl2 = CicReduction.head_beta_reduce appl2 in
+ fo_unif_subst
+ test_equality_only subst context metasenv
+ redappl1 redappl2 ugraph)
+ | _ -> raise exn)))