| C.Meta (i, _), C.Meta (j, _) when i > j ->
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
- raise (U.UnificationFailure "Inference.unification.unif")
+ raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
)
| _, C.Meta _ -> unif subst menv t s
| C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
- raise (U.UnificationFailure "Inference.unification.unif")
+ raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
| C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
try
List.fold_left2
(fun (subst', menv) s t -> unif subst' menv s t)
(subst, menv) tls tlt
with Invalid_argument _ ->
- raise (U.UnificationFailure "Inference.unification.unif")
+ raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
)
- | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+ | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
in
let subst, menv = unif [] metasenv t1 t2 in
let menv =