X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=c9d68d9deccfe96770cf888097cfcc1797ec6a20;hb=2e4a77477a9b809d9c1197e0693d2cdd43258570;hp=b016eb85f6141cc7445bb75dcdcc306d5657c4c3;hpb=4b16cd90528e372205d9537b974e3d948ef85802;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index b016eb85f..c9d68d9de 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -298,8 +298,7 @@ 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 _ 
-     | CicUniv.UniverseInconsistency _ ) when n > 0 ->
+     with CicUnification.UnificationFailure _ when n > 0 ->
       add_one_argument (n - 1)
     in
      add_one_argument goal_arity
@@ -337,7 +336,6 @@ let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
   with 
   | CicUnification.UnificationFailure msg
   | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
-  | CicUniv.UniverseInconsistency msg  -> raise (Fail (lazy msg))
 
 (* ALB *)
 let apply_tac_verbose ~term status =