]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
lddl update with the disambiguated "grundlagen"
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index d51af0bfb742b66e32af98e90ab47baad0cc5edc..584dc776a7b8d4a0d533c1b69a1ebce7e2f01414 100644 (file)
@@ -133,7 +133,8 @@ let export_entity pp_term (ra, na, u, b) =
       | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
       | E.Void   -> assert false
    in
+   let opts = if !G.si then "si" else "" in
    let shp = H.string_of_graph () in
-   let attrs = [xmlns; "hierarchy", shp] in
+   let attrs = [xmlns; "hierarchy", shp; "options", opts] in
    tag obj_root attrs ~contents out 0;
    close_out och