CicUniv.UniverseInconsistency that should be properly
captured and transformed into a tyepchecking error.
try
new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
termty n
try
new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
termty n
- with CicUnification.UnificationFailure _ when n > 0 ->
+ with (CicUnification.UnificationFailure _
+ | CicUniv.UniverseInconsistency _ ) when n > 0 ->
add_one_argument (n - 1)
in
add_one_argument goal_arity
add_one_argument (n - 1)
in
add_one_argument goal_arity
(* TODO cacciare anche altre eccezioni? *)
with
| CicUnification.UnificationFailure msg
(* TODO cacciare anche altre eccezioni? *)
with
| CicUnification.UnificationFailure msg
- | CicTypeChecker.TypeCheckerFailure msg ->
- raise (Fail msg)
+ | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
+ | CicUniv.UniverseInconsistency msg -> raise (Fail (lazy msg))
(* ALB *)
let apply_tac_verbose ~term status =
(* ALB *)
let apply_tac_verbose ~term status =