From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Nov 2005 16:16:49 +0000 (+0000)
Subject: More informative error messages.
X-Git-Tag: V_0_7_2_3~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ff3bc8b7c911ff19e9335995428351f6c38494e9;p=helm.git

More informative error messages.
---

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