X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=21bf072781c43cbfd3595090fe41f282e01febd2;hb=ff3bc8b7c911ff19e9335995428351f6c38494e9;hp=681ed492979851c963abbbf27ad9b3f181008a10;hpb=a8a60abba413c68ee65f3322f6b4028af34ed9e6;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 681ed4929..21bf07278 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -392,12 +392,13 @@ and type_of_aux' metasenv context t ugraph =
                   let search = CoercGraph.look_for_coercion in
                   let boh = search coercion_src coercion_tgt in
                   (match boh with
-                  | CoercGraph.NoCoercion ->
-                      raise (RefineFailure (lazy "no coercion"))
+                  | CoercGraph.NoCoercion
                   | CoercGraph.NotHandled _ -> 
-                      raise (RefineFailure (lazy "not a sort in PI"))
+                     raise
+                      (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
                   | CoercGraph.NotMetaClosed -> 
-                      raise (Uncertain (lazy "Coercions on metas 1"))
+                     raise
+                      (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
                   | CoercGraph.SomeCoercion c -> 
                       Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
             in