All the tactics have been ported to use the objects in LibraryObjects.

[helm.git] / helm / ocaml / cic / libraryObjects.ml

diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml
index d9fb88f6bf1b9cd9e41bcbbb35a7c84288cb0361..f7613fe1949789b496cc7820d583d3d774c91620 100644 (file)
--- a/helm/ocaml/cic/libraryObjects.ml
+++ b/helm/ocaml/cic/libraryObjects.ml
@@ -57,3 +57,7 @@ let trans_eq_URI =
  something_URI
   HelmLibraryObjects.Logic.trans_eq_URI
   MatitaLibraryObjects.Equality.trans_eq_URI
+
+let true_URI = MatitaLibraryObjects.Logic.true_URI
+let false_URI = MatitaLibraryObjects.Logic.false_URI
+let absurd_URI = MatitaLibraryObjects.Logic.absurd_URI