X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=4a6e6cadf798ef6fd16c154da24d513a4520a968;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=c5f775253a004bce33c6ea393fb5f3877dfa52d6;hpb=c80afcec268c6b6037c039f00b97274483632843;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index c5f775253..4a6e6cadf 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -880,6 +880,13 @@ and type_of_aux' metasenv context t ugraph =
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
 
+let type_of_aux' metasenv context term ugraph =
+  try 
+    type_of_aux' metasenv context term ugraph
+  with 
+    CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+    
+
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =
  try