uses CicMetaSubst.ppterm where needed

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 59ccc9ae907b4912f9674f59f7b57e3d4cf1f155..c23aada3d5b40909b284ce40af0adf9aec04c9fc 100644 (file)
--- 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")