From 45ca0fe459f75004c26e133d4cbf4659b62fd4df Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 17:03:12 +0000 Subject: [PATCH] uses CicMetaSubst.ppterm where needed --- helm/ocaml/cic_unification/cicUnification.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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") -- 2.39.2