]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/marks.mli
- new attributes system
[helm.git] / helm / software / helena / src / common / marks.mli
index ff5a681093d790adeafa7a01f7916d9fd0895e78..b4bafe680eb692c03914ade7437caf0de56ecf99 100644 (file)
@@ -9,8 +9,10 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val locations: unit -> int
+type mark
 
-val new_location: unit -> int 
+val marks: unit -> int
 
-val new_mark: unit -> Entity.attr
+val new_mark: unit -> mark 
+
+val to_string: mark -> string