]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/librarySync.ml
Axioms are not allowed with the syntax: "axiom name: type.".
[helm.git] / components / library / librarySync.ml
index 2dcd6a8b9c8b4c4aae69a4ccadd4cf81c8529b75..a09baafe1a99fe8e3fdc1aeed08451bbc706dd9d 100644 (file)
@@ -84,7 +84,7 @@ let save_object_to_disk uri obj ugraph univlist =
   (univgraphuri,xmlunivgraphpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
-       None,None -> []
+       None,_ -> []
      | Some bodyxml,Some bodyuri->
          ensure_path_exists xmlbodypath;
          Xml.pp ~gzip:true bodyxml (Some xmlbodypath);