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

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

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