Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib) et suppression Stock

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

2 files changed, 169 insertions, 156 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 518b98006..fec7fb701 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -132,7 +132,7 @@ let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
 let exact t = exact_time (Tactics.refine t)
 
-let unfold s = Tactics.unfold_in_concl [[], s]
+let unfold s = Tactics.unfold_in_concl [[], Lazy.force s]
  
 (*** fin de EST-CE QUE CES FONCTIONS NE SONT PAS AILLEURS DANS LE CODE ?? *)
 (****************************************************************)
@@ -212,135 +212,136 @@ let recognize_number t =
  This is the right way to access to Coq constants in tactics ML code *)
 
 let constant dir s =
-  Declare.global_absolute_reference
-    (make_path ("Coq"::"Zarith"::dir) (id_of_string s) CCI)
+  let dir = "Coq"::dir in
+  try 
+    Declare.global_reference_in_absolute_module dir (id_of_string s)
+  with Not_found ->
+    anomaly ("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir s)))
+
+let zarith_constant dir = constant ("Zarith"::dir)
 
 (* fast_integer *)
-let coq_xH = lazy (constant ["fast_integer"] "xH")
-let coq_xO = lazy (constant ["fast_integer"] "xO")
-let coq_xI = lazy (constant ["fast_integer"] "xI")
-let coq_ZERO = lazy (constant ["fast_integer"] "ZERO")
-let coq_POS = lazy (constant ["fast_integer"] "POS")
-let coq_NEG = lazy (constant ["fast_integer"]  "NEG")
-let coq_Z = lazy (constant ["fast_integer"] "Z")
-let coq_relation = lazy (constant ["fast_integer"] "relation")
-let coq_SUPERIEUR = lazy (constant ["fast_integer"] "SUPERIEUR")
-let coq_INFEEIEUR = lazy (constant ["fast_integer"] "INFERIEUR")
-let coq_EGAL = lazy (constant ["fast_integer"] "EGAL")
-let coq_Zplus = lazy (constant ["fast_integer"] "Zplus")
-let coq_Zmult = lazy (constant ["fast_integer"] "Zmult")
-let coq_Zopp = lazy (constant ["fast_integer"] "Zopp")
+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 (constant ["zarith_aux"] "Zminus")
-let coq_Zs = lazy (constant ["zarith_aux"] "Zs")
-let coq_Zgt = lazy (constant ["zarith_aux"] "Zgt")
-let coq_Zle = lazy (constant ["zarith_aux"] "Zle")
-let coq_inject_nat = lazy (constant ["zarith_aux"] "inject_nat")
+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 (constant ["auxiliary"] "inj_plus")
-let coq_inj_mult = lazy (constant ["auxiliary"] "inj_mult")
-let coq_inj_minus1 = lazy (constant ["auxiliary"] "inj_minus1")
-let coq_inj_minus2 = lazy (constant ["auxiliary"] "inj_minus2")
-let coq_inj_S = lazy (constant ["auxiliary"] "inj_S")
-let coq_inj_le = lazy (constant ["auxiliary"] "inj_le")
-let coq_inj_lt = lazy (constant ["auxiliary"] "inj_lt")
-let coq_inj_ge = lazy (constant ["auxiliary"] "inj_ge")
-let coq_inj_gt = lazy (constant ["auxiliary"] "inj_gt")
-let coq_inj_neq = lazy (constant ["auxiliary"] "inj_neq")
-let coq_inj_eq = lazy (constant ["auxiliary"] "inj_eq")
-let coq_pred_of_minus = lazy (constant ["auxiliary"] "pred_of_minus")
-let coq_fast_Zplus_assoc_r = lazy (constant ["auxiliary"] "fast_Zplus_assoc_r")
-let coq_fast_Zplus_assoc_l = lazy (constant ["auxiliary"] "fast_Zplus_assoc_l")
-let coq_fast_Zmult_assoc_r = lazy (constant ["auxiliary"] "fast_Zmult_assoc_r")
-let coq_fast_Zplus_permute = lazy (constant ["auxiliary"] "fast_Zplus_permute")
-let coq_fast_Zplus_sym = lazy (constant ["auxiliary"] "fast_Zplus_sym")
-let coq_fast_Zmult_sym = lazy (constant ["auxiliary"] "fast_Zmult_sym")
-let coq_Zmult_le_approx = lazy (constant ["auxiliary"] "Zmult_le_approx")
-let coq_OMEGA1 = lazy (constant ["auxiliary"] "OMEGA1")
-let coq_OMEGA2 = lazy (constant ["auxiliary"] "OMEGA2")
-let coq_OMEGA3 = lazy (constant ["auxiliary"] "OMEGA3")
-let coq_OMEGA4 = lazy (constant ["auxiliary"] "OMEGA4")
-let coq_OMEGA5 = lazy (constant ["auxiliary"] "OMEGA5")
-let coq_OMEGA6 = lazy (constant ["auxiliary"] "OMEGA6")
-let coq_OMEGA7 = lazy (constant ["auxiliary"] "OMEGA7")
-let coq_OMEGA8 = lazy (constant ["auxiliary"] "OMEGA8")
-let coq_OMEGA9 = lazy (constant ["auxiliary"] "OMEGA9")
-let coq_fast_OMEGA10 = lazy (constant ["auxiliary"] "fast_OMEGA10")
-let coq_fast_OMEGA11 = lazy (constant ["auxiliary"] "fast_OMEGA11")
-let coq_fast_OMEGA12 = lazy (constant ["auxiliary"] "fast_OMEGA12")
-let coq_fast_OMEGA13 = lazy (constant ["auxiliary"] "fast_OMEGA13")
-let coq_fast_OMEGA14 = lazy (constant ["auxiliary"] "fast_OMEGA14")
-let coq_fast_OMEGA15 = lazy (constant ["auxiliary"] "fast_OMEGA15")
-let coq_fast_OMEGA16 = lazy (constant ["auxiliary"] "fast_OMEGA16")
-let coq_OMEGA17 = lazy (constant ["auxiliary"] "OMEGA17")
-let coq_OMEGA18 = lazy (constant ["auxiliary"] "OMEGA18")
-let coq_OMEGA19 = lazy (constant ["auxiliary"] "OMEGA19")
-let coq_OMEGA20 = lazy (constant ["auxiliary"] "OMEGA20")
-let coq_fast_Zred_factor0 = lazy (constant ["auxiliary"] "fast_Zred_factor0")
-let coq_fast_Zred_factor1 = lazy (constant ["auxiliary"] "fast_Zred_factor1")
-let coq_fast_Zred_factor2 = lazy (constant ["auxiliary"] "fast_Zred_factor2")
-let coq_fast_Zred_factor3 = lazy (constant ["auxiliary"] "fast_Zred_factor3")
-let coq_fast_Zred_factor4 = lazy (constant ["auxiliary"] "fast_Zred_factor4")
-let coq_fast_Zred_factor5 = lazy (constant ["auxiliary"] "fast_Zred_factor5")
-let coq_fast_Zred_factor6 = lazy (constant ["auxiliary"] "fast_Zred_factor6")
+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 (zarith_constant ["auxiliary"] "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 (constant ["auxiliary"] "fast_Zmult_plus_distr")
+  lazy (zarith_constant ["auxiliary"] "fast_Zmult_plus_distr")
 let coq_fast_Zmult_Zopp_left = 
-  lazy (constant ["auxiliary"] "fast_Zmult_Zopp_left")
-let coq_fast_Zopp_Zplus = lazy (constant ["auxiliary"] "fast_Zopp_Zplus")
-let coq_fast_Zopp_Zmult_r = lazy (constant ["auxiliary"] "fast_Zopp_Zmult_r")
-let coq_fast_Zopp_one = lazy (constant ["auxiliary"] "fast_Zopp_one")
-let coq_fast_Zopp_Zopp = lazy (constant ["auxiliary"] "fast_Zopp_Zopp")
-let coq_Zegal_left = lazy (constant ["auxiliary"] "Zegal_left")
-let coq_Zne_left = lazy (constant ["auxiliary"] "Zne_left")
-let coq_Zlt_left = lazy (constant ["auxiliary"] "Zlt_left")
-let coq_Zge_left = lazy (constant ["auxiliary"] "Zge_left")
-let coq_Zgt_left = lazy (constant ["auxiliary"] "Zgt_left")
-let coq_Zle_left = lazy (constant ["auxiliary"] "Zle_left")
-let coq_eq_ind_r = lazy (constant ["auxiliary"] "eq_ind_r")
-let coq_new_var = lazy (constant ["auxiliary"] "new_var")
-let coq_intro_Z = lazy (constant ["auxiliary"] "intro_Z")
-let coq_dec_or = lazy (constant ["auxiliary"] "dec_or")
-let coq_dec_and = lazy (constant ["auxiliary"] "dec_and")
-let coq_dec_imp = lazy (constant ["auxiliary"] "dec_imp")
-let coq_dec_not = lazy (constant ["auxiliary"] "dec_not")
-let coq_dec_eq_nat = lazy (constant ["auxiliary"] "dec_eq_nat")
-let coq_dec_eq = lazy (constant ["auxiliary"] "dec_eq")
-let coq_dec_Zne = lazy (constant ["auxiliary"] "dec_Zne")
-let coq_dec_Zle = lazy (constant ["auxiliary"] "dec_Zle")
-let coq_dec_Zlt = lazy (constant ["auxiliary"] "dec_Zlt")
-let coq_dec_Zgt = lazy (constant ["auxiliary"] "dec_Zgt")
-let coq_dec_Zge = lazy (constant ["auxiliary"] "dec_Zge")
-let coq_dec_le = lazy (constant ["auxiliary"] "dec_le")
-let coq_dec_lt = lazy (constant ["auxiliary"] "dec_lt")
-let coq_dec_ge = lazy (constant ["auxiliary"] "dec_ge")
-let coq_dec_gt = lazy (constant ["auxiliary"] "dec_gt")
-let coq_dec_False = lazy (constant ["auxiliary"] "dec_False")
-let coq_dec_not_not = lazy (constant ["auxiliary"] "dec_not_not")
-let coq_dec_True = lazy (constant ["auxiliary"] "dec_True")
-let coq_not_Zeq = lazy (constant ["auxiliary"] "not_Zeq")
-let coq_not_Zle = lazy (constant ["auxiliary"] "not_Zle")
-let coq_not_Zlt = lazy (constant ["auxiliary"] "not_Zlt")
-let coq_not_Zge = lazy (constant ["auxiliary"] "not_Zge")
-let coq_not_Zgt = lazy (constant ["auxiliary"] "not_Zgt")
-let coq_not_le = lazy (constant ["auxiliary"] "not_le")
-let coq_not_lt = lazy (constant ["auxiliary"] "not_lt")
-let coq_not_ge = lazy (constant ["auxiliary"] "not_ge")
-let coq_not_gt = lazy (constant ["auxiliary"] "not_gt")
-let coq_not_eq = lazy (constant ["auxiliary"] "not_eq")
-let coq_not_or = lazy (constant ["auxiliary"] "not_or")
-let coq_not_and = lazy (constant ["auxiliary"] "not_and")
-let coq_not_imp = lazy (constant ["auxiliary"] "not_imp")
-let coq_not_not = lazy (constant ["auxiliary"] "not_not")
-let coq_imp_simp = lazy (constant ["auxiliary"] "imp_simp")
-let coq_neq = lazy (constant ["auxiliary"] "neq")
-let coq_Zne = lazy (constant ["auxiliary"] "Zne")
-
-let constant dir s =
-  Declare.global_absolute_reference
-    (make_path ("Coq"::dir) (id_of_string s) CCI)
+  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_eq_ind_r = lazy (zarith_constant ["auxiliary"] "eq_ind_r")
+let coq_new_var = lazy (zarith_constant ["auxiliary"] "new_var")
+let coq_intro_Z = lazy (zarith_constant ["auxiliary"] "intro_Z")
+let coq_dec_or = lazy (zarith_constant ["auxiliary"] "dec_or")
+let coq_dec_and = lazy (zarith_constant ["auxiliary"] "dec_and")
+let coq_dec_imp = lazy (zarith_constant ["auxiliary"] "dec_imp")
+let coq_dec_not = lazy (zarith_constant ["auxiliary"] "dec_not")
+let coq_dec_eq_nat = lazy (zarith_constant ["auxiliary"] "dec_eq_nat")
+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_dec_le = lazy (zarith_constant ["auxiliary"] "dec_le")
+let coq_dec_lt = lazy (zarith_constant ["auxiliary"] "dec_lt")
+let coq_dec_ge = lazy (zarith_constant ["auxiliary"] "dec_ge")
+let coq_dec_gt = lazy (zarith_constant ["auxiliary"] "dec_gt")
+let coq_dec_False = lazy (zarith_constant ["auxiliary"] "dec_False")
+let coq_dec_not_not = lazy (zarith_constant ["auxiliary"] "dec_not_not")
+let coq_dec_True = lazy (zarith_constant ["auxiliary"] "dec_True")
+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_not_le = lazy (zarith_constant ["auxiliary"] "not_le")
+let coq_not_lt = lazy (zarith_constant ["auxiliary"] "not_lt")
+let coq_not_ge = lazy (zarith_constant ["auxiliary"] "not_ge")
+let coq_not_gt = lazy (zarith_constant ["auxiliary"] "not_gt")
+let coq_not_eq = lazy (zarith_constant ["auxiliary"] "not_eq")
+let coq_not_or = lazy (zarith_constant ["auxiliary"] "not_or")
+let coq_not_and = lazy (zarith_constant ["auxiliary"] "not_and")
+let coq_not_imp = lazy (zarith_constant ["auxiliary"] "not_imp")
+let coq_not_not = lazy (zarith_constant ["auxiliary"] "not_not")
+let coq_imp_simp = lazy (zarith_constant ["auxiliary"] "imp_simp")
+let coq_neq = lazy (zarith_constant ["auxiliary"] "neq")
+let coq_Zne = lazy (zarith_constant ["auxiliary"] "Zne")
 
 (* Peano *)
 let coq_le = lazy (constant ["Init";"Peano"] "le")
@@ -358,36 +359,46 @@ let coq_minus = lazy (constant ["Arith";"Minus"] "minus")
 let coq_le_gt_dec = lazy (constant ["Arith";"Compare_dec"] "le_gt_dec")
 
 (* Logic *)
-let coq_eq = lazy (constant ["Init";"Logic"] "eq")
-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")
+open Coqlib
+let build_coq_eq = build_coq_eq_data.eq
+(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
+
 
 (* Section paths for unfold *)
 open Closure
 let make_coq_path dir s =
-  EvalConstRef (make_path ("Coq"::dir) (id_of_string s) CCI)
-let sp_Zs = make_coq_path ["Zarith";"zarith_aux"] "Zs"
-let sp_Zminus = make_coq_path ["Zarith";"zarith_aux"] "Zminus"
-let sp_Zle = make_coq_path ["Zarith";"zarith_aux"] "Zle"
-let sp_Zgt = make_coq_path ["Zarith";"zarith_aux"] "Zgt"
-let sp_Zge = make_coq_path ["Zarith";"zarith_aux"] "Zge"
-let sp_Zlt = make_coq_path ["Zarith";"zarith_aux"] "Zlt"
-let sp_not = make_coq_path ["Init";"Logic"] "not"
+  let dir = "Coq"::dir in
+  let ref = 
+    try Nametab.locate_in_absolute_module dir (id_of_string s) 
+    with Not_found ->
+      anomaly("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir s)))
+  in
+  match ref with
+    | ConstRef sp -> EvalConstRef sp
+    | _ -> anomaly ("Coq_omega: "^
+		    (string_of_qualid (make_qualid dir s))^
+		    " is not a constant")
+
+let sp_Zs = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zs")
+let sp_Zminus = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zminus")
+let sp_Zle = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zle")
+let sp_Zgt = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zgt")
+let sp_Zge = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zge")
+let sp_Zlt = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zlt")
+let sp_not = lazy (make_coq_path ["Init";"Logic"] "not")
 
 let mk_var v = mkVar (id_of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
 let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
 let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = mkApp (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |])
+let mk_eq t1 t2 = mkApp (build_coq_eq (), [| Lazy.force coq_Z; t1; t2 |])
 let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
 let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
 let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
-let mk_and t1 t2 =  mkApp (Lazy.force coq_and, [| t1; t2 |])
-let mk_or t1 t2 =  mkApp (Lazy.force coq_or, [| t1; t2 |])
-let mk_not t = mkApp (Lazy.force coq_not, [| t |])
-let mk_eq_rel t1 t2 = mkApp (Lazy.force coq_eq,
+let mk_and t1 t2 =  mkApp (build_coq_and (), [| t1; t2 |])
+let mk_or t1 t2 =  mkApp (build_coq_or (), [| t1; t2 |])
+let mk_not t = mkApp (build_coq_not (), [| t |])
+let mk_eq_rel t1 t2 = mkApp (build_coq_eq (),
 			      [| Lazy.force coq_relation; t1; t2 |])
 let mk_inj t = mkApp (Lazy.force coq_inject_nat, [| t |])
 
@@ -1002,7 +1013,7 @@ let replay_history tactic_normalisation =
 	  let tac = shuffle_cancel p_initial e1.body in
 	  let solve_le =
             let superieur = Lazy.force coq_SUPERIEUR in
-            let not_sup_sup = mkApp (Lazy.force coq_eq, [| 
+            let not_sup_sup = mkApp (build_coq_eq (), [| 
 					Lazy.force coq_relation; 
 					Lazy.force coq_SUPERIEUR;
 					Lazy.force coq_SUPERIEUR |])
@@ -1194,7 +1205,7 @@ let replay_history tactic_normalisation =
 	  let v = unintern_id sigma in
 	  let vid = id_of_string v in
 	  let theorem =
-            mkApp (Lazy.force coq_ex, [| 
+            mkApp (build_coq_ex (), [| 
 		      Lazy.force coq_Z;
 		      mkLambda
 			(Name(id_of_string v),
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 81434acd1..b3421c969 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -26,8 +26,11 @@ let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
 let constant dir s =
-  Declare.global_absolute_reference
-    (make_path ("Coq"::"ring"::dir) (id_of_string s) CCI)
+  let dir = "Coq"::"ring"::dir in
+  try 
+    Declare.global_reference_in_absolute_module dir (id_of_string s)
+  with Not_found ->
+    anomaly ("Ring: cannot find "^(string_of_qualid (make_qualid dir s)))
 
 (* Ring_theory *)
 
@@ -85,15 +88,14 @@ let coq_aspolynomial_normalize_ok =
 let coq_apolynomial_normalize_ok = 
   lazy (constant ["Ring_abstract"] "apolynomial_normalize_ok")
 
-let logic_constant dir s =
-  Declare.global_absolute_reference
-    (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI)
+(* 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
+*)
 
-(* Logic *)
-let coq_f_equal2 = lazy (logic_constant ["Logic"] "f_equal2")
-let coq_eq = lazy (logic_constant ["Logic"] "eq")
-let coq_eqT = lazy (logic_constant ["Logic_Type"] "eqT")
-let coq_sym_eqT = lazy (logic_constant ["Logic_Type"] "sym_eqT")
 
 (*********** Useful types and functions ************)
 
@@ -564,10 +566,10 @@ let raw_polynom th op lc gl =
              (tclORELSE
                (h_exact c'i_eq_c''i)
                (h_exact (mkAppA
-                 [| Lazy.force coq_sym_eqT; th.th_a; c'''i; ci; c'i_eq_c''i |]))
+                 [| build_coq_sym_eqT (); th.th_a; c'''i; ci; c'i_eq_c''i |]))
              ) 
 	     (tclTHENS 
-	       (elim_type (mkAppA [| Lazy.force coq_eqT; th.th_a; c'''i; ci |]))
+	       (elim_type (mkAppA [| build_coq_eqT (); th.th_a; c'''i; ci |]))
                [ tac ;
                  h_exact c'i_eq_c''i
                ]
@@ -583,10 +585,10 @@ let guess_eq_tac th =
 	polynom_unfold_tac
 	(tclREPEAT 
 	   (tclORELSE 
-	      (apply (mkAppA [| Lazy.force coq_f_equal2;
+	      (apply (mkAppA [| build_coq_f_equal2 ();
 				th.th_a; th.th_a; th.th_a;
 				th.th_plus |])) 
-	      (apply (mkAppA [| Lazy.force coq_f_equal2;
+	      (apply (mkAppA [| build_coq_f_equal2 ();
 				th.th_a; th.th_a; th.th_a; 
 				th.th_mult |]))))))