a better error message

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 9434f523235931389762cd1f3252f61308f9e69c..e3086c80126011c9a8be1bdb32a187e45c355296 100644 (file)
--- 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