X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=413cc986cbbc6188994a2e13f0c10e407e046b31;hb=08a92d276c5477968b02f31097b6ed03185f34eb;hp=a09baafe1a99fe8e3fdc1aeed08451bbc706dd9d;hpb=9c9e979d4c45cf3b1ee01688b2c36fe49190ce98;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index a09baafe1..413cc986c 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -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