From 98fa2447804cf187f88af1fbd0fa64d5666ff5f2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 Oct 2006 14:50:40 +0000 Subject: [PATCH] This is only a temporary patch. The typecheker raises a CicUniv.UniverseInconsistency that should be properly captured and transformed into a tyepchecking error. --- components/tactics/primitiveTactics.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 16cff94d7..b016eb85f 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -298,7 +298,8 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = 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 @@ -335,8 +336,8 @@ let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status = (* 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 = -- 2.39.2