From a46560b6efd6d66fdbe0ded0555e74ea93e46360 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Apr 2007 13:15:51 +0000 Subject: [PATCH] fixed the pretty (notation aware) printer --- helm/software/matita/applyTransformation.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2