- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
-let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con"
-let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind"
-let true_uri = (bool_uri, 0, 1)
-let false_uri = (bool_uri, 0, 2)
-
-let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con"
-let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con"
-let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con"
-let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con"
-let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con"
-let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con"
-let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con"