[coqlib] Rebindable Coqlib namespace.

We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.

This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.

Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

2 files changed, 190 insertions, 157 deletions

diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index dc86a98998..9593e1225c 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -267,3 +267,49 @@ Proof.
   intros n; exists (Z.of_nat n); split; trivial.
   rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg.
 Qed.
+
+Register fast_Zplus_assoc_reverse as plugins.omega.fast_Zplus_assoc_reverse.
+Register fast_Zplus_assoc as plugins.omega.fast_Zplus_assoc.
+Register fast_Zmult_assoc_reverse as plugins.omega.fast_Zmult_assoc_reverse.
+Register fast_Zplus_permute as plugins.omega.fast_Zplus_permute.
+Register fast_Zplus_comm as plugins.omega.fast_Zplus_comm.
+Register fast_Zmult_comm as plugins.omega.fast_Zmult_comm.
+
+Register OMEGA1 as plugins.omega.OMEGA1.
+Register OMEGA2 as plugins.omega.OMEGA2.
+Register OMEGA3 as plugins.omega.OMEGA3.
+Register OMEGA4 as plugins.omega.OMEGA4.
+Register OMEGA5 as plugins.omega.OMEGA5.
+Register OMEGA6 as plugins.omega.OMEGA6.
+Register OMEGA7 as plugins.omega.OMEGA7.
+Register OMEGA8 as plugins.omega.OMEGA8.
+Register OMEGA9 as plugins.omega.OMEGA9.
+Register fast_OMEGA10 as plugins.omega.fast_OMEGA10.
+Register fast_OMEGA11 as plugins.omega.fast_OMEGA11.
+Register fast_OMEGA12 as plugins.omega.fast_OMEGA12.
+Register fast_OMEGA13 as plugins.omega.fast_OMEGA13.
+Register fast_OMEGA14 as plugins.omega.fast_OMEGA14.
+Register fast_OMEGA15 as plugins.omega.fast_OMEGA15.
+Register fast_OMEGA16 as plugins.omega.fast_OMEGA16.
+Register OMEGA17 as plugins.omega.OMEGA17.
+Register OMEGA18 as plugins.omega.OMEGA18.
+Register OMEGA19 as plugins.omega.OMEGA19.
+Register OMEGA20 as plugins.omega.OMEGA20.
+
+Register fast_Zred_factor0 as plugins.omega.fast_Zred_factor0.
+Register fast_Zred_factor1 as plugins.omega.fast_Zred_factor1.
+Register fast_Zred_factor2 as plugins.omega.fast_Zred_factor2.
+Register fast_Zred_factor3 as plugins.omega.fast_Zred_factor3.
+Register fast_Zred_factor4 as plugins.omega.fast_Zred_factor4.
+Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5.
+Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6.
+
+Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l.
+Register fast_Zmult_opp_comm as plugins.omega.fast_Zmult_opp_comm.
+Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr.
+Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r.
+Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1.
+Register fast_Zopp_involutive as plugins.omega.fast_Zopp_involutive.
+
+Register new_var as plugins.omega.new_var.
+Register intro_Z as plugins.omega.intro_Z.
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index abae6940fa..f55458de8d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -193,172 +193,159 @@ let reset_all () =
  To use the constant Zplus, one must type "Lazy.force coq_Zplus"
  This is the right way to access to Coq constants in tactics ML code *)
 
-open Coqlib
-
-let logic_dir = ["Coq";"Logic";"Decidable"]
-let coq_modules =
-  init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
-    @ [["Coq"; "omega"; "OmegaLemmas"]]
-
-let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s)
-let init_constant = gen_constant_in_modules "Omega" init_modules
-let constant = gen_constant_in_modules "Omega" coq_modules
-
-let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]]
-let zbase_constant =
-  gen_constant_in_modules "Omega" [["Coq";"ZArith";"BinInt"]]
+let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr)
 
 
 (* Zarith *)
-let coq_xH = lazy (constant "xH")
-let coq_xO = lazy (constant "xO")
-let coq_xI = lazy (constant "xI")
-let coq_Z0 = lazy (constant "Z0")
-let coq_Zpos = lazy (constant "Zpos")
-let coq_Zneg = lazy (constant "Zneg")
-let coq_Z = lazy (constant "Z")
-let coq_comparison = lazy (constant "comparison")
-let coq_Gt = lazy (constant "Gt")
-let coq_Zplus = lazy (zbase_constant "Z.add")
-let coq_Zmult = lazy (zbase_constant "Z.mul")
-let coq_Zopp = lazy (zbase_constant "Z.opp")
-let coq_Zminus = lazy (zbase_constant "Z.sub")
-let coq_Zsucc = lazy (zbase_constant "Z.succ")
-let coq_Zpred = lazy (zbase_constant "Z.pred")
-let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat")
-let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add")
-let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul")
-let coq_inj_minus1 = lazy (z_constant "Nat2Z.inj_sub")
-let coq_inj_minus2 = lazy (constant "inj_minus2")
-let coq_inj_S = lazy (z_constant "Nat2Z.inj_succ")
-let coq_inj_le = lazy (z_constant "Znat.inj_le")
-let coq_inj_lt = lazy (z_constant "Znat.inj_lt")
-let coq_inj_ge = lazy (z_constant "Znat.inj_ge")
-let coq_inj_gt = lazy (z_constant "Znat.inj_gt")
-let coq_inj_neq = lazy (z_constant "inj_neq")
-let coq_inj_eq = lazy (z_constant "inj_eq")
-let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse")
-let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc")
-let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse")
-let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute")
-let coq_fast_Zplus_comm = lazy (constant "fast_Zplus_comm")
-let coq_fast_Zmult_comm = lazy (constant "fast_Zmult_comm")
-let coq_Zmult_le_approx = lazy (constant "Zmult_le_approx")
-let coq_OMEGA1 = lazy (constant "OMEGA1")
-let coq_OMEGA2 = lazy (constant "OMEGA2")
-let coq_OMEGA3 = lazy (constant "OMEGA3")
-let coq_OMEGA4 = lazy (constant "OMEGA4")
-let coq_OMEGA5 = lazy (constant "OMEGA5")
-let coq_OMEGA6 = lazy (constant "OMEGA6")
-let coq_OMEGA7 = lazy (constant "OMEGA7")
-let coq_OMEGA8 = lazy (constant "OMEGA8")
-let coq_OMEGA9 = lazy (constant "OMEGA9")
-let coq_fast_OMEGA10 = lazy (constant "fast_OMEGA10")
-let coq_fast_OMEGA11 = lazy (constant "fast_OMEGA11")
-let coq_fast_OMEGA12 = lazy (constant "fast_OMEGA12")
-let coq_fast_OMEGA13 = lazy (constant "fast_OMEGA13")
-let coq_fast_OMEGA14 = lazy (constant "fast_OMEGA14")
-let coq_fast_OMEGA15 = lazy (constant "fast_OMEGA15")
-let coq_fast_OMEGA16 = lazy (constant "fast_OMEGA16")
-let coq_OMEGA17 = lazy (constant "OMEGA17")
-let coq_OMEGA18 = lazy (constant "OMEGA18")
-let coq_OMEGA19 = lazy (constant "OMEGA19")
-let coq_OMEGA20 = lazy (constant "OMEGA20")
-let coq_fast_Zred_factor0 = lazy (constant "fast_Zred_factor0")
-let coq_fast_Zred_factor1 = lazy (constant "fast_Zred_factor1")
-let coq_fast_Zred_factor2 = lazy (constant "fast_Zred_factor2")
-let coq_fast_Zred_factor3 = lazy (constant "fast_Zred_factor3")
-let coq_fast_Zred_factor4 = lazy (constant "fast_Zred_factor4")
-let coq_fast_Zred_factor5 = lazy (constant "fast_Zred_factor5")
-let coq_fast_Zred_factor6 = lazy (constant "fast_Zred_factor6")
-let coq_fast_Zmult_plus_distr_l = lazy (constant "fast_Zmult_plus_distr_l")
-let coq_fast_Zmult_opp_comm =  lazy (constant "fast_Zmult_opp_comm")
-let coq_fast_Zopp_plus_distr =   lazy (constant "fast_Zopp_plus_distr")
-let coq_fast_Zopp_mult_distr_r = lazy (constant "fast_Zopp_mult_distr_r")
-let coq_fast_Zopp_eq_mult_neg_1 =  lazy (constant "fast_Zopp_eq_mult_neg_1")
-let coq_fast_Zopp_involutive = lazy (constant "fast_Zopp_involutive")
-let coq_Zegal_left = lazy (constant "Zegal_left")
-let coq_Zne_left = lazy (constant "Zne_left")
-let coq_Zlt_left = lazy (constant "Zlt_left")
-let coq_Zge_left = lazy (constant "Zge_left")
-let coq_Zgt_left = lazy (constant "Zgt_left")
-let coq_Zle_left = lazy (constant "Zle_left")
-let coq_new_var = lazy (constant "new_var")
-let coq_intro_Z = lazy (constant "intro_Z")
-
-let coq_dec_eq = lazy (zbase_constant "Z.eq_decidable")
-let coq_dec_Zne = lazy (constant "dec_Zne")
-let coq_dec_Zle = lazy (zbase_constant "Z.le_decidable")
-let coq_dec_Zlt = lazy (zbase_constant "Z.lt_decidable")
-let coq_dec_Zgt = lazy (constant "dec_Zgt")
-let coq_dec_Zge = lazy (constant "dec_Zge")
-
-let coq_not_Zeq = lazy (constant "not_Zeq")
-let coq_not_Zne = lazy (constant "not_Zne")
-let coq_Znot_le_gt = lazy (constant "Znot_le_gt")
-let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge")
-let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
-let coq_Znot_gt_le = lazy (constant "Znot_gt_le")
-let coq_neq = lazy (constant "neq")
-let coq_Zne = lazy (constant "Zne")
-let coq_Zle = lazy (zbase_constant "Z.le")
-let coq_Zgt = lazy (zbase_constant "Z.gt")
-let coq_Zge = lazy (zbase_constant "Z.ge")
-let coq_Zlt = lazy (zbase_constant "Z.lt")
+let coq_xH = gen_constant "num.pos.xH"
+let coq_xO = gen_constant "num.pos.xO"
+let coq_xI = gen_constant "num.pos.xI"
+let coq_Z0 = gen_constant "num.Z.Z0"
+let coq_Zpos = gen_constant "num.Z.Zpos"
+let coq_Zneg = gen_constant "num.Z.Zneg"
+let coq_Z = gen_constant "num.Z.type"
+let coq_comparison = gen_constant "core.comparison.type"
+let coq_Gt = gen_constant "core.comparison.Gt"
+let coq_Zplus = gen_constant "num.Z.add"
+let coq_Zmult = gen_constant "num.Z.mul"
+let coq_Zopp = gen_constant "num.Z.opp"
+let coq_Zminus = gen_constant "num.Z.sub"
+let coq_Zsucc = gen_constant "num.Z.succ"
+let coq_Zpred = gen_constant "num.Z.pred"
+let coq_Z_of_nat = gen_constant "num.Z.of_nat"
+let coq_inj_plus = gen_constant "num.Nat2Z.inj_add"
+let coq_inj_mult = gen_constant "num.Nat2Z.inj_mul"
+let coq_inj_minus1 = gen_constant "num.Nat2Z.inj_sub"
+let coq_inj_minus2 = gen_constant "plugins.omega.inj_minus2"
+let coq_inj_S = gen_constant "num.Nat2Z.inj_succ"
+let coq_inj_eq = gen_constant "plugins.omega.inj_eq"
+let coq_inj_neq = gen_constant "plugins.omega.inj_neq"
+let coq_inj_le = gen_constant "plugins.omega.inj_le"
+let coq_inj_lt = gen_constant "plugins.omega.inj_lt"
+let coq_inj_ge = gen_constant "plugins.omega.inj_ge"
+let coq_inj_gt = gen_constant "plugins.omega.inj_gt"
+let coq_fast_Zplus_assoc_reverse = gen_constant "plugins.omega.fast_Zplus_assoc_reverse"
+let coq_fast_Zplus_assoc = gen_constant "plugins.omega.fast_Zplus_assoc"
+let coq_fast_Zmult_assoc_reverse = gen_constant "plugins.omega.fast_Zmult_assoc_reverse"
+let coq_fast_Zplus_permute = gen_constant "plugins.omega.fast_Zplus_permute"
+let coq_fast_Zplus_comm = gen_constant "plugins.omega.fast_Zplus_comm"
+let coq_fast_Zmult_comm = gen_constant "plugins.omega.fast_Zmult_comm"
+let coq_Zmult_le_approx = gen_constant "plugins.omega.Zmult_le_approx"
+let coq_OMEGA1 = gen_constant "plugins.omega.OMEGA1"
+let coq_OMEGA2 = gen_constant "plugins.omega.OMEGA2"
+let coq_OMEGA3 = gen_constant "plugins.omega.OMEGA3"
+let coq_OMEGA4 = gen_constant "plugins.omega.OMEGA4"
+let coq_OMEGA5 = gen_constant "plugins.omega.OMEGA5"
+let coq_OMEGA6 = gen_constant "plugins.omega.OMEGA6"
+let coq_OMEGA7 = gen_constant "plugins.omega.OMEGA7"
+let coq_OMEGA8 = gen_constant "plugins.omega.OMEGA8"
+let coq_OMEGA9 = gen_constant "plugins.omega.OMEGA9"
+let coq_fast_OMEGA10 = gen_constant "plugins.omega.fast_OMEGA10"
+let coq_fast_OMEGA11 = gen_constant "plugins.omega.fast_OMEGA11"
+let coq_fast_OMEGA12 = gen_constant "plugins.omega.fast_OMEGA12"
+let coq_fast_OMEGA13 = gen_constant "plugins.omega.fast_OMEGA13"
+let coq_fast_OMEGA14 = gen_constant "plugins.omega.fast_OMEGA14"
+let coq_fast_OMEGA15 = gen_constant "plugins.omega.fast_OMEGA15"
+let coq_fast_OMEGA16 = gen_constant "plugins.omega.fast_OMEGA16"
+let coq_OMEGA17 = gen_constant "plugins.omega.OMEGA17"
+let coq_OMEGA18 = gen_constant "plugins.omega.OMEGA18"
+let coq_OMEGA19 = gen_constant "plugins.omega.OMEGA19"
+let coq_OMEGA20 = gen_constant "plugins.omega.OMEGA20"
+let coq_fast_Zred_factor0 = gen_constant "plugins.omega.fast_Zred_factor0"
+let coq_fast_Zred_factor1 = gen_constant "plugins.omega.fast_Zred_factor1"
+let coq_fast_Zred_factor2 = gen_constant "plugins.omega.fast_Zred_factor2"
+let coq_fast_Zred_factor3 = gen_constant "plugins.omega.fast_Zred_factor3"
+let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4"
+let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5"
+let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6"
+let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l"
+let coq_fast_Zmult_opp_comm =  gen_constant "plugins.omega.fast_Zmult_opp_comm"
+let coq_fast_Zopp_plus_distr =   gen_constant "plugins.omega.fast_Zopp_plus_distr"
+let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r"
+let coq_fast_Zopp_eq_mult_neg_1 =  gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1"
+let coq_fast_Zopp_involutive = gen_constant "plugins.omega.fast_Zopp_involutive"
+let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left"
+let coq_Zne_left = gen_constant "plugins.omega.Zne_left"
+let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left"
+let coq_Zge_left = gen_constant "plugins.omega.Zge_left"
+let coq_Zgt_left = gen_constant "plugins.omega.Zgt_left"
+let coq_Zle_left = gen_constant "plugins.omega.Zle_left"
+let coq_new_var = gen_constant "plugins.omega.new_var"
+let coq_intro_Z = gen_constant "plugins.omega.intro_Z"
+
+let coq_dec_eq = gen_constant "num.Z.eq_decidable"
+let coq_dec_Zne = gen_constant "plugins.omega.dec_Zne"
+let coq_dec_Zle = gen_constant "num.Z.le_decidable"
+let coq_dec_Zlt = gen_constant "num.Z.lt_decidable"
+let coq_dec_Zgt = gen_constant "plugins.omega.dec_Zgt"
+let coq_dec_Zge = gen_constant "plugins.omega.dec_Zge"
+
+let coq_not_Zeq = gen_constant "plugins.omega.not_Zeq"
+let coq_not_Zne = gen_constant "plugins.omega.not_Zne"
+let coq_Znot_le_gt = gen_constant "plugins.omega.Znot_le_gt"
+let coq_Znot_lt_ge = gen_constant "plugins.omega.Znot_lt_ge"
+let coq_Znot_ge_lt = gen_constant "plugins.omega.Znot_ge_lt"
+let coq_Znot_gt_le = gen_constant "plugins.omega.Znot_gt_le"
+let coq_neq = gen_constant "plugins.omega.neq"
+let coq_Zne = gen_constant "plugins.omega.Zne"
+let coq_Zle = gen_constant "num.Z.le"
+let coq_Zlt = gen_constant "num.Z.lt"
+let coq_Zge = gen_constant "num.Z.ge"
+let coq_Zgt = gen_constant "num.Z.gt"
 
 (* Peano/Datatypes *)
-let coq_le = lazy (init_constant "le")
-let coq_lt = lazy (init_constant "lt")
-let coq_ge = lazy (init_constant "ge")
-let coq_gt = lazy (init_constant "gt")
-let coq_minus = lazy (init_constant "Nat.sub")
-let coq_plus = lazy (init_constant "Nat.add")
-let coq_mult = lazy (init_constant "Nat.mul")
-let coq_pred = lazy (init_constant "Nat.pred")
-let coq_nat = lazy (init_constant "nat")
-let coq_S = lazy (init_constant "S")
-let coq_O = lazy (init_constant "O")
+let coq_nat = gen_constant "num.nat.type"
+let coq_O = gen_constant "num.nat.O"
+let coq_S = gen_constant "num.nat.S"
+let coq_le = gen_constant "num.nat.le"
+let coq_lt = gen_constant "num.nat.lt"
+let coq_ge = gen_constant "num.nat.ge"
+let coq_gt = gen_constant "num.nat.gt"
+let coq_plus = gen_constant "num.nat.add"
+let coq_minus = gen_constant "num.nat.sub"
+let coq_mult = gen_constant "num.nat.mul"
+let coq_pred = gen_constant "num.nat.pred"
 
 (* Compare_dec/Peano_dec/Minus *)
-let coq_pred_of_minus = lazy (constant "pred_of_minus")
-let coq_le_gt_dec = lazy (constant "le_gt_dec")
-let coq_dec_eq_nat = lazy (constant "dec_eq_nat")
-let coq_dec_le = lazy (constant "dec_le")
-let coq_dec_lt = lazy (constant "dec_lt")
-let coq_dec_ge = lazy (constant "dec_ge")
-let coq_dec_gt = lazy (constant "dec_gt")
-let coq_not_eq = lazy (constant "not_eq")
-let coq_not_le = lazy (constant "not_le")
-let coq_not_lt = lazy (constant "not_lt")
-let coq_not_ge = lazy (constant "not_ge")
-let coq_not_gt = lazy (constant "not_gt")
+let coq_pred_of_minus = gen_constant "num.nat.pred_of_minus"
+let coq_le_gt_dec = gen_constant "num.nat.le_gt_dec"
+let coq_dec_eq_nat = gen_constant "num.nat.eq_dec"
+let coq_dec_le = gen_constant "num.nat.dec_le"
+let coq_dec_lt = gen_constant "num.nat.dec_lt"
+let coq_dec_ge = gen_constant "num.nat.dec_ge"
+let coq_dec_gt = gen_constant "num.nat.dec_gt"
+let coq_not_eq = gen_constant "num.nat.not_eq"
+let coq_not_le = gen_constant "num.nat.not_le"
+let coq_not_lt = gen_constant "num.nat.not_lt"
+let coq_not_ge = gen_constant "num.nat.not_ge"
+let coq_not_gt = gen_constant "num.nat.not_gt"
 
 (* Logic/Decidable *)
-let coq_eq_ind_r = lazy (constant "eq_ind_r")
-
-let coq_dec_or = lazy (constant "dec_or")
-let coq_dec_and = lazy (constant "dec_and")
-let coq_dec_imp = lazy (constant "dec_imp")
-let coq_dec_iff = lazy (constant "dec_iff")
-let coq_dec_not = lazy (constant "dec_not")
-let coq_dec_False = lazy (constant "dec_False")
-let coq_dec_not_not = lazy (constant "dec_not_not")
-let coq_dec_True = lazy (constant "dec_True")
-
-let coq_not_or = lazy (constant "not_or")
-let coq_not_and = lazy (constant "not_and")
-let coq_not_imp = lazy (constant "not_imp")
-let coq_not_iff = lazy (constant "not_iff")
-let coq_not_not = lazy (constant "not_not")
-let coq_imp_simp = lazy (constant "imp_simp")
-let coq_iff = lazy (constant "iff")
-let coq_not = lazy (init_constant "not")
-let coq_and = lazy (init_constant "and")
-let coq_or = lazy (init_constant "or")
-let coq_eq = lazy (init_constant "eq")
-let coq_ex = lazy (init_constant "ex")
-let coq_False = lazy (init_constant "False")
-let coq_True = lazy (init_constant "True")
+let coq_eq_ind_r = gen_constant "core.eq.ind_r"
+
+let coq_dec_or = gen_constant "core.dec.or"
+let coq_dec_and = gen_constant "core.dec.and"
+let coq_dec_imp = gen_constant "core.dec.imp"
+let coq_dec_iff = gen_constant "core.dec.iff"
+let coq_dec_not = gen_constant "core.dec.not"
+let coq_dec_False = gen_constant "core.dec.False"
+let coq_dec_not_not = gen_constant "core.dec.not_not"
+let coq_dec_True = gen_constant "core.dec.True"
+
+let coq_not_or = gen_constant "core.dec.not_or"
+let coq_not_and = gen_constant "core.dec.not_and"
+let coq_not_imp = gen_constant "core.dec.not_imp"
+let coq_not_iff = gen_constant "core.dec.not_iff"
+let coq_not_not = gen_constant "core.dec.dec_not_not"
+let coq_imp_simp = gen_constant "core.dec.imp_simp"
+let coq_iff = gen_constant "core.iff.type"
+let coq_not = gen_constant "core.not.type"
+let coq_and = gen_constant "core.and.type"
+let coq_or = gen_constant "core.or.type"
+let coq_eq = gen_constant "core.eq.type"
+let coq_ex = gen_constant "core.ex.type"
+let coq_False = gen_constant "core.False.type"
+let coq_True = gen_constant "core.True.type"
 
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)