Error message fixed.

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 06398da9a5e3dafa1fa3e89545d8e65f3d5d5f38..55781422c0d031c249910222e22bfe1d354eb187 100644 (file)
--- 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'')))