X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fgrafite2%2FgrafiteTypes.mli;h=361a00825e2ee50c1a1fd0a541645c33338860d4;hb=55ba0a660f91e491e904dad63b14ddf2bcc2754d;hp=17544d5bda1c2220fb321f7ca83aa03ef77d68f5;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/grafite2/grafiteTypes.mli b/helm/ocaml/grafite2/grafiteTypes.mli
index 17544d5bd..361a00825 100644
--- a/helm/ocaml/grafite2/grafiteTypes.mli
+++ b/helm/ocaml/grafite2/grafiteTypes.mli
@@ -48,6 +48,7 @@ type status = {
   aliases: DisambiguateTypes.environment;         (** disambiguation aliases *)
   multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: GrafiteMarshal.moo;
+  metadata: LibraryNoDb.metadata list;
   proof_status: proof_status;                             (** logical status *)
   options: options;
   objects: UriManager.uri list;  (** in-scope objects *)
@@ -59,7 +60,7 @@ val dump_status : status -> unit
 
   (** list is not reversed, head command will be the first emitted *)
 val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
-val add_moo_metadata: GrafiteAst.metadata list -> status -> status
+val add_metadata: LibraryNoDb.metadata list -> status -> status
 
 val get_option : status -> string -> option_value
 val get_string_option : status -> string -> string