From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 Oct 2006 14:50:40 +0000 (+0000)
Subject: This is only a temporary patch. The typecheker raises a
X-Git-Tag: 0.4.95@7852~869
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98fa2447804cf187f88af1fbd0fa64d5666ff5f2;p=helm.git

This is only a temporary patch. The typecheker raises a
CicUniv.UniverseInconsistency that should be properly
captured and transformed into a tyepchecking error.
---

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 =