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

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

diff --git a/helm/ocaml/cic/matitaLibraryObjects.ml b/helm/ocaml/cic/matitaLibraryObjects.ml
index 33129ce4c072fb61bca49349492820c28ae261ee..0a4b4f11e035fc32e8d97e2d27a8b8d52a0dfb11 100644 (file)
--- a/helm/ocaml/cic/matitaLibraryObjects.ml
+++ b/helm/ocaml/cic/matitaLibraryObjects.ml
@@ -33,3 +33,10 @@ module Equality =
     let sym_eq_URI = uri "cic:/matita/equality/sym_eq.con"
     let trans_eq_URI = uri "cic:/matita/equality/trans_eq.con"
   end
+
+module Logic =
+  struct
+    let true_URI = uri "cic:/matita/logic/True.ind"
+    let false_URI = uri "cic:/matita/logic/False.ind"
+    let absurd_URI = uri "cic:/matita/logic/absurd.ind"
+  end