X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FsequentPp.ml;h=c3ab41f8812ce0e94ad722fa9f235943f9a1a861;hb=fde1a6daa3aaa72c5c7536f4d2c65a3873b1c1bc;hp=df504e75a248f4a8fc5433681a9e90e33dd7adf3;hpb=b57c31a1593872c181249135bc05ebd9a72f523b;p=helm.git

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
index df504e75a..c3ab41f88 100644
--- a/helm/gTopLevel/sequentPp.ml
+++ b/helm/gTopLevel/sequentPp.ml
@@ -59,7 +59,7 @@ module XmlPp =
             match binding with
                (Some (n,(Cic.Def t as b)) as entry)
              | (Some (n,(Cic.Decl t as b)) as entry) ->
-                let acic = acic_of_cic_context context t in
+                let acic = acic_of_cic_context context t None in
                  [< s ;
                     X.xml_nempty
                      (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
@@ -74,7 +74,7 @@ module XmlPp =
          ) context ([<>],[])
        )
       in
-       let acic = acic_of_cic_context context goal in
+       let acic = acic_of_cic_context context goal None in
         X.xml_nempty "Sequent" ["no",string_of_int metano]
          [< final_s ;
             Xml.xml_nempty "Goal" []