From d8490ed760992a42639b784fc5036d775b199c3c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 Feb 2004 16:55:44 +0000 Subject: [PATCH] Error message fixed. --- helm/ocaml/cic_unification/cicRefine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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''))) -- 2.39.2