1. metadata are no longer stored in .moo files.

[helm.git] / helm / ocaml / grafite2 / matitaSync.ml

diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml
index 26ebbd03224f8e720bec51af988f10df84816e91..2424d178f896b6b46c3e444e8a0acad1c6052d29 100644 (file)
--- 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