]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/helmLibraryObjects.ml
Porting URIs to V8.0.
[helm.git] / helm / ocaml / cic / helmLibraryObjects.ml
index 83f2d36479015f3d0626c6959a9b3a640a451c2b..3ff0163d2c6880b4520af7c8698e5c66ce092a4b 100644 (file)
@@ -80,15 +80,6 @@ module Logic =
     let absurd_URI = uri "cic:/Coq/Init/Logic/absurd.con"
   end
 
-module Logic_Type =
-  struct
-    let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind"
-    let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con"
-
-    let refl_eqt = mutconstruct eqt_URI 0 1
-    let sym_eqt = const sym_eqt_URI
-  end
-
 module Datatypes =
   struct
     let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"