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"