]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/common/library.mli
new xml exportation procedure for basic_rg (10 times faster than previous). the stati...
[helm.git] / helm / software / lambda-delta / common / library.mli
index f364af329ed9621cf5da5d10bdfce52f40d41b0e..3364175bd38b1c84e123585e5bef3c3ed5832fee 100644 (file)
@@ -50,9 +50,3 @@ val arity: int -> attr
 val name: Entity.attrs -> attr
 
 val mark: Entity.attrs -> attr
-
-val old_export_entity:
-   (Format.formatter -> 'term -> unit) -> 
-   bool -> Hierarchy.graph -> 'term Entity.entity -> unit
-
-val old_name: Format.formatter -> Entity.attrs -> unit