More informative error messages.

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 681ed492979851c963abbbf27ad9b3f181008a10..21bf072781c43cbfd3595090fe41f282e01febd2 100644 (file)
--- 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