From bda4b3ee9d66b253b258da06cea8b801924b2fe7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 5 Apr 2007 13:15:51 +0000
Subject: [PATCH] fixed the pretty (notation aware) printer

---
 matita/applyTransformation.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index de87d5548..b5aa06f9d 100644
--- a/matita/applyTransformation.ml
+++ b/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
-- 
2.39.2