]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/sequentPp.ml
* Abst removed from the DTD
[helm.git] / helm / gTopLevel / sequentPp.ml
index df504e75a248f4a8fc5433681a9e90e33dd7adf3..c3ab41f8812ce0e94ad722fa9f235943f9a1a861 100644 (file)
@@ -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" []