try
new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
termty n
- with (CicUnification.UnificationFailure _
- | CicUniv.UniverseInconsistency _ ) when n > 0 ->
+ with CicUnification.UnificationFailure _ when n > 0 ->
add_one_argument (n - 1)
in
add_one_argument goal_arity
with
| CicUnification.UnificationFailure msg
| CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
- | CicUniv.UniverseInconsistency msg -> raise (Fail (lazy msg))
(* ALB *)
let apply_tac_verbose ~term status =