From: Stefano Zacchiroli <zack@upsilon.cc>
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")