Un peu plus de souplesse dans la globalisation des noms utilises par les tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 406 insertions, 337 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 8982969f1d..d30a557ba4 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -143,163 +143,169 @@ let hide_constr,find_constr,clear_tables,dump_tables =
  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 *)
 
-let constant = Coqlib.gen_constant "Omega"
-
-let arith_constant dir = constant ("Arith"::dir)
-let zarith_constant dir = constant ("ZArith"::dir)
-let logic_constant dir = constant ("Logic"::dir)
-
-(* fast_integer *)
-let coq_xH = lazy (zarith_constant ["fast_integer"] "xH")
-let coq_xO = lazy (zarith_constant ["fast_integer"] "xO")
-let coq_xI = lazy (zarith_constant ["fast_integer"] "xI")
-let coq_ZERO = lazy (zarith_constant ["fast_integer"] "ZERO")
-let coq_POS = lazy (zarith_constant ["fast_integer"] "POS")
-let coq_NEG = lazy (zarith_constant ["fast_integer"]  "NEG")
-let coq_Z = lazy (zarith_constant ["fast_integer"] "Z")
-let coq_relation = lazy (zarith_constant ["fast_integer"] "relation")
-let coq_SUPERIEUR = lazy (zarith_constant ["fast_integer"] "SUPERIEUR")
-let coq_INFEEIEUR = lazy (zarith_constant ["fast_integer"] "INFERIEUR")
-let coq_EGAL = lazy (zarith_constant ["fast_integer"] "EGAL")
-let coq_Zplus = lazy (zarith_constant ["fast_integer"] "Zplus")
-let coq_Zmult = lazy (zarith_constant ["fast_integer"] "Zmult")
-let coq_Zopp = lazy (zarith_constant ["fast_integer"] "Zopp")
-
-(* zarith_aux *)
-let coq_Zminus = lazy (zarith_constant ["zarith_aux"] "Zminus")
-let coq_Zs = lazy (zarith_constant ["zarith_aux"] "Zs")
-let coq_Zgt = lazy (zarith_constant ["zarith_aux"] "Zgt")
-let coq_Zle = lazy (zarith_constant ["zarith_aux"] "Zle")
-let coq_inject_nat = lazy (zarith_constant ["zarith_aux"] "inject_nat")
-
-(* auxiliary *)
-let coq_inj_plus = lazy (zarith_constant ["auxiliary"] "inj_plus")
-let coq_inj_mult = lazy (zarith_constant ["auxiliary"] "inj_mult")
-let coq_inj_minus1 = lazy (zarith_constant ["auxiliary"] "inj_minus1")
-let coq_inj_minus2 = lazy (zarith_constant ["auxiliary"] "inj_minus2")
-let coq_inj_S = lazy (zarith_constant ["auxiliary"] "inj_S")
-let coq_inj_le = lazy (zarith_constant ["auxiliary"] "inj_le")
-let coq_inj_lt = lazy (zarith_constant ["auxiliary"] "inj_lt")
-let coq_inj_ge = lazy (zarith_constant ["auxiliary"] "inj_ge")
-let coq_inj_gt = lazy (zarith_constant ["auxiliary"] "inj_gt")
-let coq_inj_neq = lazy (zarith_constant ["auxiliary"] "inj_neq")
-let coq_inj_eq = lazy (zarith_constant ["auxiliary"] "inj_eq")
-let coq_pred_of_minus = lazy (arith_constant ["Minus"] "pred_of_minus")
-let coq_fast_Zplus_assoc_r = lazy (zarith_constant ["auxiliary"] "fast_Zplus_assoc_r")
-let coq_fast_Zplus_assoc_l = lazy (zarith_constant ["auxiliary"] "fast_Zplus_assoc_l")
-let coq_fast_Zmult_assoc_r = lazy (zarith_constant ["auxiliary"] "fast_Zmult_assoc_r")
-let coq_fast_Zplus_permute = lazy (zarith_constant ["auxiliary"] "fast_Zplus_permute")
-let coq_fast_Zplus_sym = lazy (zarith_constant ["auxiliary"] "fast_Zplus_sym")
-let coq_fast_Zmult_sym = lazy (zarith_constant ["auxiliary"] "fast_Zmult_sym")
-let coq_Zmult_le_approx = lazy (zarith_constant ["auxiliary"] "Zmult_le_approx")
-let coq_OMEGA1 = lazy (zarith_constant ["auxiliary"] "OMEGA1")
-let coq_OMEGA2 = lazy (zarith_constant ["auxiliary"] "OMEGA2")
-let coq_OMEGA3 = lazy (zarith_constant ["auxiliary"] "OMEGA3")
-let coq_OMEGA4 = lazy (zarith_constant ["auxiliary"] "OMEGA4")
-let coq_OMEGA5 = lazy (zarith_constant ["auxiliary"] "OMEGA5")
-let coq_OMEGA6 = lazy (zarith_constant ["auxiliary"] "OMEGA6")
-let coq_OMEGA7 = lazy (zarith_constant ["auxiliary"] "OMEGA7")
-let coq_OMEGA8 = lazy (zarith_constant ["auxiliary"] "OMEGA8")
-let coq_OMEGA9 = lazy (zarith_constant ["auxiliary"] "OMEGA9")
-let coq_fast_OMEGA10 = lazy (zarith_constant ["auxiliary"] "fast_OMEGA10")
-let coq_fast_OMEGA11 = lazy (zarith_constant ["auxiliary"] "fast_OMEGA11")
-let coq_fast_OMEGA12 = lazy (zarith_constant ["auxiliary"] "fast_OMEGA12")
-let coq_fast_OMEGA13 = lazy (zarith_constant ["auxiliary"] "fast_OMEGA13")
-let coq_fast_OMEGA14 = lazy (zarith_constant ["auxiliary"] "fast_OMEGA14")
-let coq_fast_OMEGA15 = lazy (zarith_constant ["auxiliary"] "fast_OMEGA15")
-let coq_fast_OMEGA16 = lazy (zarith_constant ["auxiliary"] "fast_OMEGA16")
-let coq_OMEGA17 = lazy (zarith_constant ["auxiliary"] "OMEGA17")
-let coq_OMEGA18 = lazy (zarith_constant ["auxiliary"] "OMEGA18")
-let coq_OMEGA19 = lazy (zarith_constant ["auxiliary"] "OMEGA19")
-let coq_OMEGA20 = lazy (zarith_constant ["auxiliary"] "OMEGA20")
-let coq_fast_Zred_factor0 = lazy (zarith_constant ["auxiliary"] "fast_Zred_factor0")
-let coq_fast_Zred_factor1 = lazy (zarith_constant ["auxiliary"] "fast_Zred_factor1")
-let coq_fast_Zred_factor2 = lazy (zarith_constant ["auxiliary"] "fast_Zred_factor2")
-let coq_fast_Zred_factor3 = lazy (zarith_constant ["auxiliary"] "fast_Zred_factor3")
-let coq_fast_Zred_factor4 = lazy (zarith_constant ["auxiliary"] "fast_Zred_factor4")
-let coq_fast_Zred_factor5 = lazy (zarith_constant ["auxiliary"] "fast_Zred_factor5")
-let coq_fast_Zred_factor6 = lazy (zarith_constant ["auxiliary"] "fast_Zred_factor6")
-let coq_fast_Zmult_plus_distr =
-  lazy (zarith_constant ["auxiliary"] "fast_Zmult_plus_distr")
-let coq_fast_Zmult_Zopp_left = 
-  lazy (zarith_constant ["auxiliary"] "fast_Zmult_Zopp_left")
-let coq_fast_Zopp_Zplus = lazy (zarith_constant ["auxiliary"] "fast_Zopp_Zplus")
-let coq_fast_Zopp_Zmult_r = lazy (zarith_constant ["auxiliary"] "fast_Zopp_Zmult_r")
-let coq_fast_Zopp_one = lazy (zarith_constant ["auxiliary"] "fast_Zopp_one")
-let coq_fast_Zopp_Zopp = lazy (zarith_constant ["auxiliary"] "fast_Zopp_Zopp")
-let coq_Zegal_left = lazy (zarith_constant ["auxiliary"] "Zegal_left")
-let coq_Zne_left = lazy (zarith_constant ["auxiliary"] "Zne_left")
-let coq_Zlt_left = lazy (zarith_constant ["auxiliary"] "Zlt_left")
-let coq_Zge_left = lazy (zarith_constant ["auxiliary"] "Zge_left")
-let coq_Zgt_left = lazy (zarith_constant ["auxiliary"] "Zgt_left")
-let coq_Zle_left = lazy (zarith_constant ["auxiliary"] "Zle_left")
-let coq_new_var = lazy (zarith_constant ["auxiliary"] "new_var")
-let coq_intro_Z = lazy (zarith_constant ["auxiliary"] "intro_Z")
-
-let coq_dec_eq = lazy (zarith_constant ["auxiliary"] "dec_eq")
-let coq_dec_Zne = lazy (zarith_constant ["auxiliary"] "dec_Zne")
-let coq_dec_Zle = lazy (zarith_constant ["auxiliary"] "dec_Zle")
-let coq_dec_Zlt = lazy (zarith_constant ["auxiliary"] "dec_Zlt")
-let coq_dec_Zgt = lazy (zarith_constant ["auxiliary"] "dec_Zgt")
-let coq_dec_Zge = lazy (zarith_constant ["auxiliary"] "dec_Zge")
-
-let coq_not_Zeq = lazy (zarith_constant ["auxiliary"] "not_Zeq")
-let coq_not_Zle = lazy (zarith_constant ["auxiliary"] "not_Zle")
-let coq_not_Zlt = lazy (zarith_constant ["auxiliary"] "not_Zlt")
-let coq_not_Zge = lazy (zarith_constant ["auxiliary"] "not_Zge")
-let coq_not_Zgt = lazy (zarith_constant ["auxiliary"] "not_Zgt")
-let coq_neq = lazy (zarith_constant ["auxiliary"] "neq")
-let coq_Zne = lazy (zarith_constant ["auxiliary"] "Zne")
-let coq_Zle = lazy (zarith_constant ["zarith_aux"] "Zle")
-let coq_Zgt = lazy (zarith_constant ["zarith_aux"] "Zgt")
-let coq_Zge = lazy (zarith_constant ["zarith_aux"] "Zge")
-let coq_Zlt = lazy (zarith_constant ["zarith_aux"] "Zlt")
-
-(* Peano *)
-let coq_le = lazy (constant ["Init";"Peano"] "le")
-let coq_lt = lazy (constant ["Init";"Peano"] "lt")
-let coq_ge = lazy (constant ["Init";"Peano"] "ge")
-let coq_gt = lazy (constant ["Init";"Peano"] "gt")
-let coq_minus = lazy (constant ["Init";"Peano"] "minus")
-let coq_plus = lazy (constant ["Init";"Peano"] "plus")
-let coq_mult = lazy (constant ["Init";"Peano"] "mult")
-let coq_pred = lazy (constant ["Init";"Peano"] "pred")
-
-(* Datatypes *)
-let coq_nat = lazy (constant ["Init";"Datatypes"] "nat")
-let coq_S = lazy (constant ["Init";"Datatypes"] "S")
-let coq_O = lazy (constant ["Init";"Datatypes"] "O")
-
-(* Compare_dec *)
-let coq_le_gt_dec = lazy (constant ["Arith";"Compare_dec"] "le_gt_dec")
-let coq_dec_eq_nat = lazy (constant ["Arith";"Peano_dec"] "dec_eq_nat")
-let coq_dec_le = lazy (constant ["Arith";"Compare_dec"] "dec_le")
-let coq_dec_lt = lazy (constant ["Arith";"Compare_dec"] "dec_lt")
-let coq_dec_ge = lazy (constant ["Arith";"Compare_dec"] "dec_ge")
-let coq_dec_gt = lazy (constant ["Arith";"Compare_dec"] "dec_gt")
-let coq_not_eq = lazy (constant ["Arith";"Compare_dec"] "not_eq")
-let coq_not_le = lazy (constant ["Arith";"Compare_dec"] "not_le")
-let coq_not_lt = lazy (constant ["Arith";"Compare_dec"] "not_lt")
-let coq_not_ge = lazy (constant ["Arith";"Compare_dec"] "not_ge")
-let coq_not_gt = lazy (constant ["Arith";"Compare_dec"] "not_gt")
-
-(* Logic *)
+let init_dir = ["Coq";"Init"]
+let arith_dir = ["Coq";"Arith"]
+let logic_dir = ["Coq";"Logic"]
+let zarith_dir = ["Coq";"ZArith"]
+let coq_modules = [
+  zarith_dir@["fast_integer"];
+  zarith_dir@["zarith_aux"];
+  zarith_dir@["auxiliary"];
+  init_dir@["Datatypes"];
+  init_dir@["Peano"];
+  init_dir@["Logic"];
+  arith_dir@["Compare_dec"];
+  arith_dir@["Peano_dec"];
+  arith_dir@["Minus"];
+  logic_dir@["Decidable"]
+]
+
 open Coqlib
-let coq_eq_ind_r = lazy (constant ["Init"; "Logic"] "eq_ind_r")
-
-let coq_dec_or = lazy (logic_constant ["Decidable"] "dec_or")
-let coq_dec_and = lazy (logic_constant ["Decidable"] "dec_and")
-let coq_dec_imp = lazy (logic_constant ["Decidable"] "dec_imp")
-let coq_dec_not = lazy (logic_constant ["Decidable"] "dec_not")
-let coq_dec_False = lazy (logic_constant ["Decidable"] "dec_False")
-let coq_dec_not_not = lazy (logic_constant ["Decidable"] "dec_not_not")
-let coq_dec_True = lazy (logic_constant ["Decidable"] "dec_True")
-
-let coq_not_or = lazy (logic_constant ["Decidable"] "not_or")
-let coq_not_and = lazy (logic_constant ["Decidable"] "not_and")
-let coq_not_imp = lazy (logic_constant ["Decidable"] "not_imp")
-let coq_not_not = lazy (logic_constant ["Decidable"] "not_not")
-let coq_imp_simp = lazy (logic_constant ["Decidable"] "imp_simp")
+
+let constant = gen_constant_in_modules "Omega" coq_modules
+
+(* Zarith *)
+let coq_xH = lazy (constant "xH")
+let coq_xO = lazy (constant "xO")
+let coq_xI = lazy (constant "xI")
+let coq_ZERO = lazy (constant "ZERO")
+let coq_POS = lazy (constant "POS")
+let coq_NEG = lazy (constant  "NEG")
+let coq_Z = lazy (constant "Z")
+let coq_relation = lazy (constant "relation")
+let coq_SUPERIEUR = lazy (constant "SUPERIEUR")
+let coq_INFEEIEUR = lazy (constant "INFERIEUR")
+let coq_EGAL = lazy (constant "EGAL")
+let coq_Zplus = lazy (constant "Zplus")
+let coq_Zmult = lazy (constant "Zmult")
+let coq_Zopp = lazy (constant "Zopp")
+let coq_Zminus = lazy (constant "Zminus")
+let coq_Zs = lazy (constant "Zs")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zle = lazy (constant "Zle")
+let coq_inject_nat = lazy (constant "inject_nat")
+let coq_inj_plus = lazy (constant "inj_plus")
+let coq_inj_mult = lazy (constant "inj_mult")
+let coq_inj_minus1 = lazy (constant "inj_minus1")
+let coq_inj_minus2 = lazy (constant "inj_minus2")
+let coq_inj_S = lazy (constant "inj_S")
+let coq_inj_le = lazy (constant "inj_le")
+let coq_inj_lt = lazy (constant "inj_lt")
+let coq_inj_ge = lazy (constant "inj_ge")
+let coq_inj_gt = lazy (constant "inj_gt")
+let coq_inj_neq = lazy (constant "inj_neq")
+let coq_inj_eq = lazy (constant "inj_eq")
+let coq_fast_Zplus_assoc_r = lazy (constant "fast_Zplus_assoc_r")
+let coq_fast_Zplus_assoc_l = lazy (constant "fast_Zplus_assoc_l")
+let coq_fast_Zmult_assoc_r = lazy (constant "fast_Zmult_assoc_r")
+let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute")
+let coq_fast_Zplus_sym = lazy (constant "fast_Zplus_sym")
+let coq_fast_Zmult_sym = lazy (constant "fast_Zmult_sym")
+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 = lazy (constant "fast_Zmult_plus_distr")
+let coq_fast_Zmult_Zopp_left =  lazy (constant "fast_Zmult_Zopp_left")
+let coq_fast_Zopp_Zplus =   lazy (constant "fast_Zopp_Zplus")
+let coq_fast_Zopp_Zmult_r = lazy (constant "fast_Zopp_Zmult_r")
+let coq_fast_Zopp_one =  lazy (constant "fast_Zopp_one")
+let coq_fast_Zopp_Zopp = lazy (constant "fast_Zopp_Zopp")
+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 (constant "dec_eq")
+let coq_dec_Zne = lazy (constant "dec_Zne")
+let coq_dec_Zle = lazy (constant "dec_Zle")
+let coq_dec_Zlt = lazy (constant "dec_Zlt")
+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_Zle = lazy (constant "not_Zle")
+let coq_not_Zlt = lazy (constant "not_Zlt")
+let coq_not_Zge = lazy (constant "not_Zge")
+let coq_not_Zgt = lazy (constant "not_Zgt")
+let coq_neq = lazy (constant "neq")
+let coq_Zne = lazy (constant "Zne")
+let coq_Zle = lazy (constant "Zle")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zge = lazy (constant "Zge")
+let coq_Zlt = lazy (constant "Zlt")
+
+(* Peano/Datatypes *)
+let coq_le = lazy (constant "le")
+let coq_lt = lazy (constant "lt")
+let coq_ge = lazy (constant "ge")
+let coq_gt = lazy (constant "gt")
+let coq_minus = lazy (constant "minus")
+let coq_plus = lazy (constant "plus")
+let coq_mult = lazy (constant "mult")
+let coq_pred = lazy (constant "pred")
+let coq_nat = lazy (constant "nat")
+let coq_S = lazy (constant "S")
+let coq_O = lazy (constant "O")
+
+(* 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")
+
+(* 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_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_not = lazy (constant "not_not")
+let coq_imp_simp = lazy (constant "imp_simp")
 
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index b927cd8cba..bfad74ac49 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -38,103 +38,97 @@ open Quote
 let mt_evd = Evd.empty
 let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
 
-let constant = Coqlib.gen_constant "Ring"
+let ring_dir = ["Coq";"ring"]
+let setoids_dir = ["Coq";"Setoids"]
+
+let ring_constant = Coqlib.gen_constant_in_modules "Ring"
+  [ring_dir@["Ring_theory"];
+   ring_dir@["Setoid_ring_theory"];
+   ring_dir@["Ring_normalize"];
+   ring_dir@["Ring_abstract"];
+   setoids_dir@["Setoid"];
+   ring_dir@["Setoid_ring_normalize"]]
 
 (* Ring theory *)
-let coq_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Ring_Theory")
-let coq_Semi_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Semi_Ring_Theory")
+let coq_Ring_Theory = lazy (ring_constant "Ring_Theory")
+let coq_Semi_Ring_Theory = lazy (ring_constant "Semi_Ring_Theory")
 
 (* Setoid ring theory *)
-let coq_Setoid_Ring_Theory = lazy (constant ["ring";"Setoid_ring_theory"] "Setoid_Ring_Theory")
-let coq_Semi_Setoid_Ring_Theory = lazy (constant ["ring";"Setoid_ring_theory"] "Semi_Setoid_Ring_Theory")
+let coq_Setoid_Ring_Theory = lazy (ring_constant "Setoid_Ring_Theory")
+let coq_Semi_Setoid_Ring_Theory = lazy(ring_constant "Semi_Setoid_Ring_Theory")
 
 (* Ring normalize *)
-let coq_SPplus = lazy (constant ["ring";"Ring_normalize"] "SPplus")
-let coq_SPmult = lazy (constant ["ring";"Ring_normalize"] "SPmult")
-let coq_SPvar = lazy (constant ["ring";"Ring_normalize"] "SPvar")
-let coq_SPconst = lazy (constant ["ring";"Ring_normalize"] "SPconst")
-let coq_Pplus = lazy (constant ["ring";"Ring_normalize"] "Pplus")
-let coq_Pmult = lazy (constant ["ring";"Ring_normalize"] "Pmult")
-let coq_Pvar = lazy (constant ["ring";"Ring_normalize"] "Pvar")
-let coq_Pconst = lazy (constant ["ring";"Ring_normalize"] "Pconst")
-let coq_Popp = lazy (constant ["ring";"Ring_normalize"] "Popp")
-let coq_interp_sp = lazy (constant ["ring";"Ring_normalize"] "interp_sp")
-let coq_interp_p = lazy (constant ["ring";"Ring_normalize"] "interp_p")
-let coq_interp_cs = lazy (constant ["ring";"Ring_normalize"] "interp_cs")
-let coq_spolynomial_simplify = 
-  lazy (constant ["ring";"Ring_normalize"] "spolynomial_simplify")
-let coq_polynomial_simplify = 
-  lazy (constant ["ring";"Ring_normalize"] "polynomial_simplify")
-let coq_spolynomial_simplify_ok = 
-  lazy (constant ["ring";"Ring_normalize"] "spolynomial_simplify_ok")
-let coq_polynomial_simplify_ok = 
-  lazy (constant ["ring";"Ring_normalize"] "polynomial_simplify_ok")
+let coq_SPplus = lazy (ring_constant "SPplus")
+let coq_SPmult = lazy (ring_constant "SPmult")
+let coq_SPvar = lazy (ring_constant "SPvar")
+let coq_SPconst = lazy (ring_constant "SPconst")
+let coq_Pplus = lazy (ring_constant "Pplus")
+let coq_Pmult = lazy (ring_constant "Pmult")
+let coq_Pvar = lazy (ring_constant "Pvar")
+let coq_Pconst = lazy (ring_constant "Pconst")
+let coq_Popp = lazy (ring_constant "Popp")
+let coq_interp_sp = lazy (ring_constant "interp_sp")
+let coq_interp_p = lazy (ring_constant "interp_p")
+let coq_interp_cs = lazy (ring_constant "interp_cs")
+let coq_spolynomial_simplify = lazy (ring_constant "spolynomial_simplify")
+let coq_polynomial_simplify = lazy (ring_constant "polynomial_simplify")
+let coq_spolynomial_simplify_ok = lazy(ring_constant "spolynomial_simplify_ok")
+let coq_polynomial_simplify_ok = lazy (ring_constant "polynomial_simplify_ok")
 
 (* Setoid theory *)
-let coq_Setoid_Theory = lazy(constant ["Setoids";"Setoid"] "Setoid_Theory")
+let coq_Setoid_Theory = lazy(ring_constant "Setoid_Theory")
 
-let coq_seq_refl = lazy(constant ["Setoids";"Setoid"] "Seq_refl")
-let coq_seq_sym = lazy(constant ["Setoids";"Setoid"] "Seq_sym")
-let coq_seq_trans = lazy(constant ["Setoids";"Setoid"] "Seq_trans")
+let coq_seq_refl = lazy(ring_constant "Seq_refl")
+let coq_seq_sym = lazy(ring_constant "Seq_sym")
+let coq_seq_trans = lazy(ring_constant "Seq_trans")
 
 (* Setoid Ring normalize *)
-let coq_SetSPplus = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPplus")
-let coq_SetSPmult = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPmult")
-let coq_SetSPvar = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPvar")
-let coq_SetSPconst = lazy (constant ["ring";"Setoid_ring_normalize"] "SetSPconst")
-let coq_SetPplus = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPplus")
-let coq_SetPmult = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPmult")
-let coq_SetPvar = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPvar")
-let coq_SetPconst = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPconst")
-let coq_SetPopp = lazy (constant ["ring";"Setoid_ring_normalize"] "SetPopp")
-let coq_interp_setsp = lazy (constant ["ring";"Setoid_ring_normalize"] "interp_setsp")
-let coq_interp_setp = lazy (constant ["ring";"Setoid_ring_normalize"] "interp_setp")
-let coq_interp_setcs = lazy (constant ["ring";"Setoid_ring_normalize"] "interp_cs")
+let coq_SetSPplus = lazy (ring_constant "SetSPplus")
+let coq_SetSPmult = lazy (ring_constant "SetSPmult")
+let coq_SetSPvar = lazy (ring_constant "SetSPvar")
+let coq_SetSPconst = lazy (ring_constant "SetSPconst")
+let coq_SetPplus = lazy (ring_constant "SetPplus")
+let coq_SetPmult = lazy (ring_constant "SetPmult")
+let coq_SetPvar = lazy (ring_constant "SetPvar")
+let coq_SetPconst = lazy (ring_constant "SetPconst")
+let coq_SetPopp = lazy (ring_constant "SetPopp")
+let coq_interp_setsp = lazy (ring_constant "interp_setsp")
+let coq_interp_setp = lazy (ring_constant "interp_setp")
+let coq_interp_setcs = lazy (ring_constant "interp_cs")
 let coq_setspolynomial_simplify = 
-  lazy (constant ["ring";"Setoid_ring_normalize"] "setspolynomial_simplify")
+  lazy (ring_constant "setspolynomial_simplify")
 let coq_setpolynomial_simplify = 
-  lazy (constant ["ring";"Setoid_ring_normalize"] "setpolynomial_simplify")
+  lazy (ring_constant "setpolynomial_simplify")
 let coq_setspolynomial_simplify_ok = 
-  lazy (constant ["ring";"Setoid_ring_normalize"] "setspolynomial_simplify_ok")
+  lazy (ring_constant "setspolynomial_simplify_ok")
 let coq_setpolynomial_simplify_ok = 
-  lazy (constant ["ring";"Setoid_ring_normalize"] "setpolynomial_simplify_ok")
+  lazy (ring_constant "setpolynomial_simplify_ok")
 
 (* Ring abstract *)
-let coq_ASPplus = lazy (constant ["ring";"Ring_abstract"] "ASPplus")
-let coq_ASPmult = lazy (constant ["ring";"Ring_abstract"] "ASPmult")
-let coq_ASPvar = lazy (constant ["ring";"Ring_abstract"] "ASPvar")
-let coq_ASP0 = lazy (constant ["ring";"Ring_abstract"] "ASP0")
-let coq_ASP1 = lazy (constant ["ring";"Ring_abstract"] "ASP1")
-let coq_APplus = lazy (constant ["ring";"Ring_abstract"] "APplus")
-let coq_APmult = lazy (constant ["ring";"Ring_abstract"] "APmult")
-let coq_APvar = lazy (constant ["ring";"Ring_abstract"] "APvar")
-let coq_AP0 = lazy (constant ["ring";"Ring_abstract"] "AP0")
-let coq_AP1 = lazy (constant ["ring";"Ring_abstract"] "AP1")
-let coq_APopp = lazy (constant ["ring";"Ring_abstract"] "APopp")
-let coq_interp_asp = 
-  lazy (constant ["ring";"Ring_abstract"] "interp_asp")
-let coq_interp_ap = 
-  lazy (constant ["ring";"Ring_abstract"] "interp_ap")
- let coq_interp_acs = 
-  lazy (constant ["ring";"Ring_abstract"] "interp_acs")
-let coq_interp_sacs = 
-  lazy (constant ["ring";"Ring_abstract"] "interp_sacs")
-let coq_aspolynomial_normalize = 
-  lazy (constant ["ring";"Ring_abstract"] "aspolynomial_normalize")
-let coq_apolynomial_normalize = 
-  lazy (constant ["ring";"Ring_abstract"] "apolynomial_normalize")
+let coq_ASPplus = lazy (ring_constant "ASPplus")
+let coq_ASPmult = lazy (ring_constant "ASPmult")
+let coq_ASPvar = lazy (ring_constant "ASPvar")
+let coq_ASP0 = lazy (ring_constant "ASP0")
+let coq_ASP1 = lazy (ring_constant "ASP1")
+let coq_APplus = lazy (ring_constant "APplus")
+let coq_APmult = lazy (ring_constant "APmult")
+let coq_APvar = lazy (ring_constant "APvar")
+let coq_AP0 = lazy (ring_constant "AP0")
+let coq_AP1 = lazy (ring_constant "AP1")
+let coq_APopp = lazy (ring_constant "APopp")
+let coq_interp_asp = lazy (ring_constant "interp_asp")
+let coq_interp_ap = lazy (ring_constant "interp_ap")
+let coq_interp_acs = lazy (ring_constant "interp_acs")
+let coq_interp_sacs = lazy (ring_constant "interp_sacs")
+let coq_aspolynomial_normalize = lazy (ring_constant "aspolynomial_normalize")
+let coq_apolynomial_normalize = lazy (ring_constant "apolynomial_normalize")
 let coq_aspolynomial_normalize_ok = 
-  lazy (constant ["ring";"Ring_abstract"] "aspolynomial_normalize_ok")
+  lazy (ring_constant "aspolynomial_normalize_ok")
 let coq_apolynomial_normalize_ok = 
-  lazy (constant ["ring";"Ring_abstract"] "apolynomial_normalize_ok")
+  lazy (ring_constant "apolynomial_normalize_ok")
 
 (* Logic --> to be found in Coqlib *)
 open Coqlib
-(*
-val build_coq_f_equal2 : constr delayed
-val build_coq_eqT : constr delayed
-val build_coq_sym_eqT : constr delayed
-*)
 
 let mkLApp(fc,v) = mkApp(Lazy.force fc, v)
 
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index cbff8eea7d..28a969babc 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -62,125 +62,146 @@ let recognize_number t =
        "POS",[t] -> loop t | "NEG",[t] -> - (loop t) | "ZERO",[] -> 0
      | _ -> failwith "not a number";;
 
-let constant = Coqlib.gen_constant "Omega"
-
-let coq_xH = lazy (constant ["ZArith"; "fast_integer"] "xH")
-let coq_xO = lazy (constant ["ZArith"; "fast_integer"] "xO")
-let coq_xI = lazy (constant ["ZArith"; "fast_integer"] "xI")
-let coq_ZERO = lazy (constant ["ZArith"; "fast_integer"] "ZERO")
-let coq_POS = lazy (constant ["ZArith"; "fast_integer"] "POS")
-let coq_NEG = lazy (constant ["ZArith"; "fast_integer"] "NEG")
-let coq_Z = lazy (constant ["ZArith"; "fast_integer"] "Z")
-let coq_relation = lazy (constant ["ZArith"; "fast_integer"] "relation")
-let coq_SUPERIEUR = lazy (constant ["ZArith"; "fast_integer"] "SUPERIEUR")
-let coq_INFEEIEUR = lazy (constant ["ZArith"; "fast_integer"] "INFERIEUR")
-let coq_EGAL = lazy (constant ["ZArith"; "fast_integer"] "EGAL")
-let coq_Zplus = lazy (constant ["ZArith"; "fast_integer"] "Zplus")
-let coq_Zmult = lazy (constant ["ZArith"; "fast_integer"] "Zmult")
-let coq_Zopp = lazy (constant ["ZArith"; "fast_integer"] "Zopp")
+let init_dir = ["Coq";"Init"]
+let arith_dir = ["Coq";"Arith"]
+let logic_dir = ["Coq";"Logic"]
+let zarith_dir = ["Coq";"ZArith"]
+let list_dir = ["Coq";"Lists"]
+let coq_modules = [
+  zarith_dir@["fast_integer"];
+  zarith_dir@["zarith_aux"];
+  zarith_dir@["auxiliary"];
+  init_dir@["Datatypes"];
+  init_dir@["Peano"];
+  init_dir@["Logic"];
+  arith_dir@["Compare_dec"];
+  arith_dir@["Peano_dec"];
+  arith_dir@["Minus"];
+  logic_dir@["Decidable"];
+  list_dir@["PolyList"]
+]
+
+let constant = Coqlib.gen_constant_in_modules "ROmega" coq_modules
+
+let coq_xH = lazy (constant "xH")
+let coq_xO = lazy (constant "xO")
+let coq_xI = lazy (constant "xI")
+let coq_ZERO = lazy (constant "ZERO")
+let coq_POS = lazy (constant "POS")
+let coq_NEG = lazy (constant "NEG")
+let coq_Z = lazy (constant "Z")
+let coq_relation = lazy (constant "relation")
+let coq_SUPERIEUR = lazy (constant "SUPERIEUR")
+let coq_INFEEIEUR = lazy (constant "INFERIEUR")
+let coq_EGAL = lazy (constant "EGAL")
+let coq_Zplus = lazy (constant "Zplus")
+let coq_Zmult = lazy (constant "Zmult")
+let coq_Zopp = lazy (constant "Zopp")
 
 (* auxiliaires zarith *)
-let coq_Zminus = lazy (constant ["ZArith"; "zarith_aux"] "Zminus")
-let coq_Zs = lazy (constant ["ZArith"; "zarith_aux"] "Zs")
-let coq_Zgt = lazy (constant ["ZArith"; "zarith_aux"] "Zgt")
-let coq_Zle = lazy (constant ["ZArith"; "zarith_aux"] "Zle")
-let coq_inject_nat = lazy (constant ["ZArith"; "zarith_aux"] "inject_nat")
+let coq_Zminus = lazy (constant "Zminus")
+let coq_Zs = lazy (constant "Zs")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zle = lazy (constant "Zle")
+let coq_inject_nat = lazy (constant "inject_nat")
 
 (* Peano *)
-let coq_le = lazy(constant ["Init"; "Peano"] "le")
-let coq_gt = lazy(constant ["Init"; "Peano"] "gt")
+let coq_le = lazy(constant "le")
+let coq_gt = lazy(constant "gt")
 
 (* Datatypes *)
-let coq_nat = lazy(constant ["Init"; "Datatypes"] "nat")
-let coq_S = lazy(constant ["Init"; "Datatypes"] "S")
-let coq_O = lazy(constant ["Init"; "Datatypes"] "O")
+let coq_nat = lazy(constant "nat")
+let coq_S = lazy(constant "S")
+let coq_O = lazy(constant "O")
 
 (* Minus *)
-let coq_minus = lazy(constant ["Arith"; "Minus"] "minus")
+let coq_minus = lazy(constant "minus")
 
 (* Logic *)
-let coq_eq = lazy(constant ["Init"; "Logic"] "eq")
-let coq_refl_equal = lazy(constant ["Init"; "Logic"] "refl_equal")
-let coq_and = lazy(constant ["Init"; "Logic"] "and")
-let coq_not = lazy(constant ["Init"; "Logic"] "not")
-let coq_or = lazy(constant ["Init"; "Logic"] "or")
-let coq_ex = lazy(constant ["Init"; "Logic"] "ex")
+let coq_eq = lazy(constant "eq")
+let coq_refl_equal = lazy(constant "refl_equal")
+let coq_and = lazy(constant "and")
+let coq_not = lazy(constant "not")
+let coq_or = lazy(constant "or")
+let coq_ex = lazy(constant "ex")
 
 (* Lists *)
-let coq_cons =  lazy (constant ["Lists"; "PolyList"] "cons")
-let coq_nil =  lazy (constant ["Lists"; "PolyList"] "nil")
-
-let coq_t_nat = lazy (constant module_refl_path "Tint")
-let coq_t_plus = lazy (constant module_refl_path "Tplus")
-let coq_t_mult = lazy (constant module_refl_path "Tmult")
-let coq_t_opp = lazy (constant module_refl_path "Topp")
-let coq_t_minus = lazy (constant module_refl_path "Tminus")
-let coq_t_var = lazy (constant module_refl_path "Tvar")
-let coq_t_equal = lazy (constant module_refl_path "EqTerm")
-let coq_t_leq = lazy (constant module_refl_path "LeqTerm")
-let coq_t_geq = lazy (constant module_refl_path "GeqTerm")
-let coq_t_lt = lazy (constant module_refl_path "LtTerm")
-let coq_t_gt = lazy (constant module_refl_path "GtTerm")
-let coq_t_neq = lazy (constant module_refl_path "NeqTerm")
-
-let coq_proposition = lazy (constant module_refl_path "proposition")
-let coq_interp_sequent = lazy (constant module_refl_path "interp_goal")
-let coq_normalize_sequent = lazy (constant module_refl_path "normalize_goal")
-let coq_execute_sequent = lazy (constant module_refl_path "execute_goal")
-let coq_sequent_to_hyps = lazy (constant module_refl_path "goal_to_hyps")
+let coq_cons =  lazy (constant "cons")
+let coq_nil =  lazy (constant "nil")
+
+let romega_constant = Coqlib.gen_constant "ROmega" module_refl_path
+
+let coq_t_nat = lazy (romega_constant "Tint")
+let coq_t_plus = lazy (romega_constant "Tplus")
+let coq_t_mult = lazy (romega_constant "Tmult")
+let coq_t_opp = lazy (romega_constant "Topp")
+let coq_t_minus = lazy (romega_constant "Tminus")
+let coq_t_var = lazy (romega_constant "Tvar")
+let coq_t_equal = lazy (romega_constant "EqTerm")
+let coq_t_leq = lazy (romega_constant "LeqTerm")
+let coq_t_geq = lazy (romega_constant "GeqTerm")
+let coq_t_lt = lazy (romega_constant "LtTerm")
+let coq_t_gt = lazy (romega_constant "GtTerm")
+let coq_t_neq = lazy (romega_constant "NeqTerm")
+
+let coq_proposition = lazy (romega_constant "proposition")
+let coq_interp_sequent = lazy (romega_constant "interp_goal")
+let coq_normalize_sequent = lazy (romega_constant "normalize_goal")
+let coq_execute_sequent = lazy (romega_constant "execute_goal")
+let coq_sequent_to_hyps = lazy (romega_constant "goal_to_hyps")
 
 (* Constructors for shuffle tactic *)
-let coq_t_fusion =  lazy (constant module_refl_path "t_fusion")
-let coq_f_equal =  lazy (constant module_refl_path "F_equal")
-let coq_f_cancel =  lazy (constant module_refl_path "F_cancel")
-let coq_f_left =  lazy (constant module_refl_path "F_left")
-let coq_f_right =  lazy (constant module_refl_path "F_right")
+let coq_t_fusion =  lazy (romega_constant "t_fusion")
+let coq_f_equal =  lazy (romega_constant "F_equal")
+let coq_f_cancel =  lazy (romega_constant "F_cancel")
+let coq_f_left =  lazy (romega_constant "F_left")
+let coq_f_right =  lazy (romega_constant "F_right")
 
 (* Constructors for reordering tactics *)
-let coq_step = lazy (constant module_refl_path "step")
-let coq_c_do_both = lazy (constant module_refl_path "C_DO_BOTH")
-let coq_c_do_left = lazy (constant module_refl_path "C_LEFT")
-let coq_c_do_right = lazy (constant module_refl_path "C_RIGHT")
-let coq_c_do_seq = lazy (constant module_refl_path "C_SEQ")
-let coq_c_nop = lazy (constant module_refl_path "C_NOP")
-let coq_c_opp_plus = lazy (constant module_refl_path "C_OPP_PLUS")
-let coq_c_opp_opp = lazy (constant module_refl_path "C_OPP_OPP")
-let coq_c_opp_mult_r = lazy (constant module_refl_path "C_OPP_MULT_R")
-let coq_c_opp_one = lazy (constant module_refl_path "C_OPP_ONE")
-let coq_c_reduce = lazy (constant module_refl_path "C_REDUCE")
-let coq_c_mult_plus_distr = lazy (constant module_refl_path "C_MULT_PLUS_DISTR")
-let coq_c_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
-let coq_c_mult_assoc_r = lazy (constant module_refl_path "C_MULT_ASSOC_R")
-let coq_c_plus_assoc_r = lazy (constant module_refl_path "C_PLUS_ASSOC_R")
-let coq_c_plus_assoc_l = lazy (constant module_refl_path "C_PLUS_ASSOC_L")
-let coq_c_plus_permute = lazy (constant module_refl_path "C_PLUS_PERMUTE")
-let coq_c_plus_sym = lazy (constant module_refl_path "C_PLUS_SYM")
-let coq_c_red0 = lazy (constant module_refl_path "C_RED0")
-let coq_c_red1 = lazy (constant module_refl_path "C_RED1")
-let coq_c_red2 = lazy (constant module_refl_path "C_RED2")
-let coq_c_red3 = lazy (constant module_refl_path "C_RED3")
-let coq_c_red4 = lazy (constant module_refl_path "C_RED4")
-let coq_c_red5 = lazy (constant module_refl_path "C_RED5")
-let coq_c_red6 = lazy (constant module_refl_path "C_RED6")
-let coq_c_mult_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
+let coq_step = lazy (romega_constant "step")
+let coq_c_do_both = lazy (romega_constant "C_DO_BOTH")
+let coq_c_do_left = lazy (romega_constant "C_LEFT")
+let coq_c_do_right = lazy (romega_constant "C_RIGHT")
+let coq_c_do_seq = lazy (romega_constant "C_SEQ")
+let coq_c_nop = lazy (romega_constant "C_NOP")
+let coq_c_opp_plus = lazy (romega_constant "C_OPP_PLUS")
+let coq_c_opp_opp = lazy (romega_constant "C_OPP_OPP")
+let coq_c_opp_mult_r = lazy (romega_constant "C_OPP_MULT_R")
+let coq_c_opp_one = lazy (romega_constant "C_OPP_ONE")
+let coq_c_reduce = lazy (romega_constant "C_REDUCE")
+let coq_c_mult_plus_distr = lazy (romega_constant "C_MULT_PLUS_DISTR")
+let coq_c_opp_left = lazy (romega_constant "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_r = lazy (romega_constant "C_MULT_ASSOC_R")
+let coq_c_plus_assoc_r = lazy (romega_constant "C_PLUS_ASSOC_R")
+let coq_c_plus_assoc_l = lazy (romega_constant "C_PLUS_ASSOC_L")
+let coq_c_plus_permute = lazy (romega_constant "C_PLUS_PERMUTE")
+let coq_c_plus_sym = lazy (romega_constant "C_PLUS_SYM")
+let coq_c_red0 = lazy (romega_constant "C_RED0")
+let coq_c_red1 = lazy (romega_constant "C_RED1")
+let coq_c_red2 = lazy (romega_constant "C_RED2")
+let coq_c_red3 = lazy (romega_constant "C_RED3")
+let coq_c_red4 = lazy (romega_constant "C_RED4")
+let coq_c_red5 = lazy (romega_constant "C_RED5")
+let coq_c_red6 = lazy (romega_constant "C_RED6")
+let coq_c_mult_opp_left = lazy (romega_constant "C_MULT_OPP_LEFT")
 let coq_c_mult_assoc_reduced = 
-  lazy (constant module_refl_path "C_MULT_ASSOC_REDUCED")
-let coq_c_minus = lazy (constant module_refl_path "C_MINUS")
-let coq_c_mult_sym = lazy (constant module_refl_path "C_MULT_SYM")
-
-let coq_s_constant_not_nul = lazy (constant module_refl_path "O_CONSTANT_NOT_NUL")
-let coq_s_constant_neg = lazy (constant module_refl_path "O_CONSTANT_NEG")
-let coq_s_div_approx = lazy (constant module_refl_path "O_DIV_APPROX")
-let coq_s_not_exact_divide = lazy (constant module_refl_path "O_NOT_EXACT_DIVIDE")
-let coq_s_exact_divide = lazy (constant module_refl_path "O_EXACT_DIVIDE")
-let coq_s_sum = lazy (constant module_refl_path "O_SUM")
-let coq_s_state = lazy (constant module_refl_path "O_STATE")
-let coq_s_contradiction = lazy (constant module_refl_path "O_CONTRADICTION")
-let coq_s_merge_eq = lazy (constant module_refl_path "O_MERGE_EQ")
-let coq_s_split_ineq =lazy (constant module_refl_path "O_SPLIT_INEQ")
-let coq_s_constant_nul =lazy (constant module_refl_path "O_CONSTANT_NUL")
-let coq_s_negate_contradict =lazy (constant module_refl_path "O_NEGATE_CONTRADICT")
-let coq_s_negate_contradict_inv =lazy (constant module_refl_path "O_NEGATE_CONTRADICT_INV")
+  lazy (romega_constant "C_MULT_ASSOC_REDUCED")
+let coq_c_minus = lazy (romega_constant "C_MINUS")
+let coq_c_mult_sym = lazy (romega_constant "C_MULT_SYM")
+
+let coq_s_constant_not_nul = lazy (romega_constant "O_CONSTANT_NOT_NUL")
+let coq_s_constant_neg = lazy (romega_constant "O_CONSTANT_NEG")
+let coq_s_div_approx = lazy (romega_constant "O_DIV_APPROX")
+let coq_s_not_exact_divide = lazy (romega_constant "O_NOT_EXACT_DIVIDE")
+let coq_s_exact_divide = lazy (romega_constant "O_EXACT_DIVIDE")
+let coq_s_sum = lazy (romega_constant "O_SUM")
+let coq_s_state = lazy (romega_constant "O_STATE")
+let coq_s_contradiction = lazy (romega_constant "O_CONTRADICTION")
+let coq_s_merge_eq = lazy (romega_constant "O_MERGE_EQ")
+let coq_s_split_ineq =lazy (romega_constant "O_SPLIT_INEQ")
+let coq_s_constant_nul =lazy (romega_constant "O_CONSTANT_NUL")
+let coq_s_negate_contradict =lazy (romega_constant "O_NEGATE_CONTRADICT")
+let coq_s_negate_contradict_inv =lazy (romega_constant "O_NEGATE_CONTRADICT_INV")
 
 (* \subsection{Construction d'expressions} *)
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index e02dfbb190..963d391e1a 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -9,6 +9,7 @@
 (* $Id$ *)
 
 open Util
+open Pp
 open Names
 open Term
 open Libnames
@@ -20,18 +21,60 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 let gen_reference locstr dir s =
   let dir = make_dir ("Coq"::dir) in
   let id = Constrextern.id_of_v7_string s in
-  try 
-    Nametab.absolute_reference (Libnames.make_path dir id)
+  let sp = Libnames.make_path dir id in
+  try
+    Nametab.absolute_reference sp
   with Not_found ->
-    anomaly (locstr^": cannot find "^(string_of_qualid (make_qualid dir id)))
-
+    anomaly (locstr^": cannot find "^(string_of_path sp))
+    
 let gen_constant locstr dir s = 
   constr_of_reference (gen_reference locstr dir s)
 
+let list_try_find f = 
+  let rec try_find_f = function
+    | [] -> raise Not_found
+    | h::t -> try f h with Not_found -> try_find_f t
+  in 
+  try_find_f
+
+let gen_constant_in_modules locstr dirs s =
+  let dirs = List.map make_dir dirs in
+  let id = Constrextern.id_of_v7_string s in
+  try
+    list_try_find
+      (fun dir ->
+	constr_of_reference
+	  (Nametab.absolute_reference (Libnames.make_path dir id)))
+      dirs
+  with Not_found ->
+    anomalylabstrm "" (str (locstr^": cannot find "^s^
+    " in module"^(if List.length dirs > 1 then "s " else " ")) ++
+    prlist_with_sep pr_coma pr_dirpath dirs)
+
 let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s
 
 let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s  
 
+let zarith_dir = ["Coq";"ZArith"]
+let zarith_base_modules = [
+  zarith_dir@["fast_integer"];
+  zarith_dir@["zarith_aux"];
+  zarith_dir@["auxiliary"];
+  zarith_dir@["ZArith_dec"];
+  zarith_dir@["Zmisc"];
+  zarith_dir@["Wf_Z"]
+]
+
+let init_dir = ["Coq";"Init"]
+let init_modules = [
+  init_dir@["Datatypes"];
+  init_dir@["Logic"];
+  init_dir@["Specif"];
+  init_dir@["Logic_Type"];
+  init_dir@["Peano"];
+  init_dir@["Wf"]
+]
+  
 let coq_id = id_of_string "Coq"
 let init_id = id_of_string "Init"
 let arith_id = id_of_string "Arith"
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 0eff556623..cd169dbcd9 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -25,6 +25,11 @@ open Pattern
 val gen_reference : string->string list -> string -> global_reference
 val gen_constant : string->string list -> string -> constr
 
+(* Search in several modules (not prefixed by "Coq") *)
+val gen_constant_in_modules : string->string list list-> string -> constr
+val zarith_base_modules : string list list
+val init_modules : string list list
+
 (*s Global references *)
 
 (* Modules *)