]> matita.cs.unibo.it Git - helm.git/commitdiff
a better error message
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 23 Jan 2004 16:37:00 +0000 (16:37 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 23 Jan 2004 16:37:00 +0000 (16:37 +0000)
helm/ocaml/cic_unification/cicRefine.ml

index 9434f523235931389762cd1f3252f61308f9e69c..e3086c80126011c9a8be1bdb32a187e45c355296 100644 (file)
@@ -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