-let assert_applicability err f ~si m u w v =
- let f mu = function
- | B.Sort _ -> error1 err "not a function type" m u
- | B.Bind (B.Abst (_, u), _) ->
- let err _ = error3 err m v w ~mu u in
- R.are_convertible err f ~si mu u m w
- | _ -> assert false
- in
- R.xwhd f m u
+let assert_applicability err f st m u w v =
+ match R.xwhd st m u with
+ | _, B.Sort _ -> error1 err "not a function type" m u
+ | mu, B.Bind (_, B.Abst u, _) ->
+ if R.are_convertible st mu u m w then f () else
+ error3 err m v w ~mu u
+ | _ -> assert false (**)