]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed the pretty (notation aware) printer
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 5 Apr 2007 13:15:51 +0000 (13:15 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 5 Apr 2007 13:15:51 +0000 (13:15 +0000)
helm/software/matita/applyTransformation.ml

index de87d55489c1ce31ef855550301a976c08c1c68f..b5aa06f9d1d87ffd0e74b3a5023884af3be90b1c 100644 (file)
@@ -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