From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 5 Apr 2007 13:15:51 +0000 (+0000)
Subject: fixed the pretty (notation aware) printer
X-Git-Tag: make_still_working~6407
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a46560b6efd6d66fdbe0ded0555e74ea93e46360;p=helm.git

fixed the pretty (notation aware) printer
---

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index de87d5548..b5aa06f9d 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -107,6 +107,7 @@ ignore (
   (fun ~metasenv subst term context ->
     try
      let context' = CicMetaSubst.apply_subst_context subst context in
+     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
      let term' = CicMetaSubst.apply_subst subst term in
      let res = txt_of_cic_term 30 metasenv context' term' in
       if String.contains res '\n' then