- let fo_unif_subst =
- let (lower,upper) =
- match t1,t2 with
- C.Meta (n,_), C.Meta (m,_) when n < m ->
- (fun t1 t2 -> t1), (fun t1 t2 -> t2)
- | _, C.Meta _ ->
- (fun t1 t2 -> t1), (fun t1 t2 -> t2)
- | _,_ ->
- (fun t1 t2 -> t2), (fun t1 t2 -> t1)
- in
- fun subst context metasenv m1 m2 ->
+ 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 subst context metasenv m1 m2 =