From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 18:21:36 +0000 (+0000) Subject: Improved error messages. X-Git-Tag: V_0_2_3~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15325be7092744101275e469f90c3faeab778fea;p=helm.git Improved error messages. --- diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index b64d8f4bb..77b376d63 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -419,7 +419,7 @@ and type_of_aux' metasenv context t = | Some t,Some (_,C.Def (ct,_)) -> (try CicUnification.fo_unif_subst subst context metasenv t ct - with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct)))) + with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | Some t,Some (_,C.Decl ct) -> let inferredty,subst',metasenv' = type_of_aux subst metasenv context t @@ -427,7 +427,7 @@ and type_of_aux' metasenv context t = (try CicUnification.fo_unif_subst subst' context metasenv' inferredty ct - with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct)))) + with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | None, Some _ -> raise (NotRefinable (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"