]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteSync.ml
Bad variable name fixed.
[helm.git] / helm / software / components / grafite_engine / grafiteSync.ml
index ca29d39fcc1a159459bd96ab9bc42d0e52772a76..7946b4a1e211ec3a0b769ba49f81f1ca8594b591 100644 (file)
@@ -174,10 +174,10 @@ let initial_status lexicon_status baseuri =
  (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus
 ;;
 
-let init baseuri =
+let init lexicon_status =
   CoercDb.restore CoercDb.empty_coerc_db;
   LibraryObjects.reset_defaults ();
-  initial_status baseuri
+  initial_status lexicon_status
   ;;
 let pop () =
   LibrarySync.pop ();