X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=55781422c0d031c249910222e22bfe1d354eb187;hb=d8490ed760992a42639b784fc5036d775b199c3c;hp=06398da9a5e3dafa1fa3e89545d8e65f3d5d5f38;hpb=d48c8c8358c9dc4083254d847d7c4ee13d47e6ab;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 06398da9a..55781422c 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -482,7 +482,7 @@ and type_of_aux' metasenv context t =
           t2'',subst,metasenv
      | (_,_) ->
          raise (NotRefinable (sprintf
-          "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
+          "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
           (CicPp.ppterm t2'')))