1. the default for the default equality/absurd/true/false URIs used to be

[helm.git] / helm / software / components / library / librarySync.ml

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 2dcd6a8b9c8b4c4aae69a4ccadd4cf81c8529b75..413cc986cbbc6188994a2e13f0c10e407e046b31 100644 (file)
--- 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