X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite2%2FmatitaSync.ml;h=2424d178f896b6b46c3e444e8a0acad1c6052d29;hb=dbb9f64a437b4abda0b9f47a527ab6135d596e28;hp=26ebbd03224f8e720bec51af988f10df84816e91;hpb=024819eeb7fcd370114ceb3dffc7907db92ab640;p=helm.git

diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml
index 26ebbd032..2424d178f 100644
--- a/helm/ocaml/grafite2/matitaSync.ml
+++ b/helm/ocaml/grafite2/matitaSync.ml
@@ -56,7 +56,7 @@ let set_proof_aliases status new_aliases =
     (function
     | GrafiteAst.Ident_alias (_, suri) ->
         let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
-        Some (GrafiteAst.Dependency buri)
+        Some (LibraryNoDb.Dependency buri)
     | _ -> None)
  in
  let aliases =
@@ -75,7 +75,7 @@ let set_proof_aliases status new_aliases =
      DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
    in
    let status = add_moo_content (commands_of_aliases aliases) new_status in
-   let status = add_moo_metadata (deps_of_aliases aliases) status in
+   let status = add_metadata (deps_of_aliases aliases) status in
    status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs