let uri = UriManager.uri_of_string

let const ?(subst = []) uri = Cic.Const (uri, subst)
let var ?(subst = []) uri = Cic.Var (uri, subst)
let mutconstruct ?(subst = []) uri typeno consno =
  Cic.MutConstruct (uri, typeno, consno, subst)

module Logic =
  struct
    let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind"
    let true_URI = uri "cic:/Coq/Init/Logic/True.ind"
    let false_URI = uri "cic:/Coq/Init/Logic/False.ind"
  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"
    let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind"

    let trueb = mutconstruct bool_URI 0 1
    let falseb = mutconstruct bool_URI 0 2
    let zero = mutconstruct nat_URI 0 1
    let succ = mutconstruct nat_URI 0 2
  end

module Reals =
  struct
    let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con"
    let rplus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rplus.con"
    let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con"
    let ropp_URI = uri "cic:/Coq/Reals/Rdefinitions/Ropp.con"
    let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con"
    let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con"
    let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"

    let r = const r_URI
    let rplus = const rplus_URI
    let rmult = const rmult_URI
    let ropp = const ropp_URI
    let r0 = const r0_URI
    let r1 = const r1_URI
    let rtheory = const rtheory_URI
  end