From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 17:03:12 +0000 (+0000) Subject: uses CicMetaSubst.ppterm where needed X-Git-Tag: V_0_2_3~104 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=45ca0fe459f75004c26e133d4cbf4659b62fd4df;p=helm.git uses CicMetaSubst.ppterm where needed --- diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 59ccc9ae9..c23aada3d 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -38,7 +38,7 @@ let type_of_aux' metasenv subst context term = raise (AssertFailure ((sprintf "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms" - (CicPp.ppterm (CicMetaSubst.apply_subst subst term)) + (CicMetaSubst.ppterm subst term) (CicMetaSubst.ppcontext subst context) msg))) (* NUOVA UNIFICAZIONE *) @@ -219,11 +219,11 @@ let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;; let fo_unif_subst subst context metasenv t1 t2 = let enrich_msg msg = sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" - (CicPp.ppterm (CicMetaSubst.apply_subst subst t1)) + (CicMetaSubst.ppterm subst t1) (try CicPp.ppterm (type_of_aux' metasenv subst context t1) with _ -> "MALFORMED") - (CicPp.ppterm (CicMetaSubst.apply_subst subst t2)) + (CicMetaSubst.ppterm subst t2) (try CicPp.ppterm (type_of_aux' metasenv subst context t2) with _ -> "MALFORMED")