From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 26 Feb 2004 16:55:44 +0000 (+0000)
Subject: Error message fixed.
X-Git-Tag: v0_0_4~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d8490ed760992a42639b784fc5036d775b199c3c;p=helm.git

Error message fixed.
---

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'')))