X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=413cc986cbbc6188994a2e13f0c10e407e046b31;hb=cc3ab906b631ef0edb4402cb622fc3fa96682717;hp=2dcd6a8b9c8b4c4aae69a4ccadd4cf81c8529b75;hpb=894802b5e169f37e5390683b6b29b4fbb4be1083;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 2dcd6a8b9..413cc986c 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -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);
@@ -336,7 +336,7 @@ let add_obj refinement_toolkit uri obj =
     | Cic.InductiveDefinition (_,_,_,attrs) ->
         uris := !uris @ 
           generate_elimination_principles uri refinement_toolkit;
-	      (* uris := !uris @ generate_inversion refinement_toolkit uri obj; *)
+	uris := !uris @ generate_inversion refinement_toolkit uri obj;
         let rec get_record_attrs =
           function
           | [] -> None