From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 23 Jan 2004 16:37:00 +0000 (+0000)
Subject: a better error message
X-Git-Tag: V_0_2_3~164
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a385fe3bdae148cc8ba6eeac56d77cf13baa7e12;p=helm.git

a better error message
---

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 9434f5232..e3086c801 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+open Printf
+
 exception Impossible of int;;
 exception NotRefinable of string;;
 exception Uncertain of string;;
@@ -440,16 +442,11 @@ and type_of_aux' metasenv context t =
            CicMkImplicit.identity_relocation_list_for_metavariable context
          in
          C.Meta (idx, irl), subst, metasenv'
-(*
-       raise
-        (Uncertain
-          ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
-           CicPp.ppterm t2''))
-*)
      | (_,_) ->
-       raise
-        (NotRefinable
-         ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
+         raise (NotRefinable (sprintf
+          "Two types were expected, found %s of type %s and %s of type %s"
+          (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
+          (CicPp.ppterm t2'')))
 
  and eat_prods subst metasenv context hetype =
   function