+ let swap =
+ match t1,t2 with
+ C.Meta (n,_), C.Meta (m,_) when n < m -> false
+ | _, C.Meta _ -> false
+ | _,_ -> true
+ in
+ let lower = fun x y -> if swap then y else x in
+ let upper = fun x y -> if swap then x else y in
+ let fo_unif_subst_ordered
+ test_equality_only subst context metasenv m1 m2 =
+ fo_unif_subst test_equality_only subst context metasenv
+ (lower m1 m2) (upper m1 m2)
+ in