Remplacement des hacks pour les noms longs par un appel à Declare.global_qualified_reference

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

3 files changed, 195 insertions, 228 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index ca241ecd2..bdf4544f9 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -15,6 +15,7 @@ open Proof_type
 open Ast
 open Names
 open Term
+open Environ
 open Sign
 open Inductive
 open Tacmach
@@ -206,181 +207,154 @@ let recognize_number t =
  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 sp id = 
-  Declare.global_sp_reference (path_of_string sp) (id_of_string id)
+let constant dir id = 
+  Declare.global_qualified_reference
+    (make_path dir (id_of_string id) CCI)
 
 (* fast_integer *)
-let coq_xH = lazy (constant "#fast_integer#positive.cci" "xH")
-let coq_xO = lazy (constant "#fast_integer#positive.cci" "xO")
-let coq_xI = lazy (constant "#fast_integer#positive.cci" "xI")
-let coq_ZERO = lazy (constant "#fast_integer#Z.cci" "ZERO")
-let coq_POS = lazy (constant "#fast_integer#Z.cci" "POS")
-let coq_NEG = lazy (constant "#fast_integer#Z.cci"  "NEG")
-let coq_Z = lazy (constant "#fast_integer#Z.cci" "Z")
-let coq_relation = lazy (constant "#fast_integer#relation.cci" "relation")
-let coq_SUPERIEUR = lazy (constant "#fast_integer#relation.cci" "SUPERIEUR")
-let coq_INFEEIEUR = lazy (constant "#fast_integer#relation.cci" "INFERIEUR")
-let coq_EGAL = lazy (constant "#fast_integer#relation.cci" "EGAL")
-let coq_Zplus = lazy (constant "#fast_integer#Zplus.cci" "Zplus")
-let coq_Zmult = lazy (constant "#fast_integer#Zmult.cci" "Zmult")
-let coq_Zopp = lazy (constant "#fast_integer#Zopp.cci" "Zopp")
+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")
 
 (* zarith_aux *)
-let coq_Zminus = lazy (constant "#zarith_aux#Zminus.cci" "Zminus")
-let coq_Zs = lazy (constant "#zarith_aux#Zs.cci" "Zs")
-let coq_Zgt = lazy (constant "#zarith_aux#Zgt.cci" "Zgt")
-let coq_Zle = lazy (constant "#zarith_aux#Zle.cci" "Zle")
-let coq_inject_nat = lazy (constant "#zarith_aux#inject_nat.cci" "inject_nat")
+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")
 
 (* auxiliary *)
-let coq_inj_plus = lazy (constant "#auxiliary#inj_plus.cci" "inj_plus")
-let coq_inj_mult = lazy (constant "#auxiliary#inj_mult.cci" "inj_mult")
-let coq_inj_minus1 = lazy (constant "#auxiliary#inj_minus1.cci" "inj_minus1")
-let coq_inj_minus2 = lazy (constant "#auxiliary#inj_minus2.cci" "inj_minus2")
-let coq_inj_S = lazy (constant "#auxiliary#inj_S.cci" "inj_S")
-let coq_inj_le = lazy (constant "#auxiliary#inj_le.cci" "inj_le")
-let coq_inj_lt = lazy (constant "#auxiliary#inj_lt.cci" "inj_lt")
-let coq_inj_ge = lazy (constant "#auxiliary#inj_ge.cci" "inj_ge")
-let coq_inj_gt = lazy (constant "#auxiliary#inj_gt.cci" "inj_gt")
-let coq_inj_neq = lazy (constant "#auxiliary#inj_neq.cci" "inj_neq")
-let coq_inj_eq = lazy (constant "#auxiliary#inj_eq.cci" "inj_eq")
-let coq_pred_of_minus = 
-  lazy (constant "#auxiliary#pred_of_minus.cci" "pred_of_minus")
-let coq_fast_Zplus_assoc_r = 
-  lazy (constant "#auxiliary#fast_Zplus_assoc_r.cci" "fast_Zplus_assoc_r")
-let coq_fast_Zplus_assoc_l = 
-  lazy (constant "#auxiliary#fast_Zplus_assoc_l.cci" "fast_Zplus_assoc_l")
-let coq_fast_Zmult_assoc_r = 
-  lazy (constant "#auxiliary#fast_Zmult_assoc_r.cci" "fast_Zmult_assoc_r")
-let coq_fast_Zplus_permute = 
-  lazy (constant "#auxiliary#fast_Zplus_permute.cci" "fast_Zplus_permute")
-let coq_fast_Zplus_sym = 
-  lazy (constant "#auxiliary#fast_Zplus_sym.cci" "fast_Zplus_sym")
-let coq_fast_Zmult_sym = 
-  lazy (constant "#auxiliary#fast_Zmult_sym.cci" "fast_Zmult_sym")
-let coq_Zmult_le_approx = 
-  lazy (constant "#auxiliary#Zmult_le_approx.cci" "Zmult_le_approx")
-let coq_OMEGA1 = lazy (constant "#auxiliary#OMEGA1.cci" "OMEGA1")
-let coq_OMEGA2 = lazy (constant "#auxiliary#OMEGA2.cci" "OMEGA2")
-let coq_OMEGA3 = lazy (constant "#auxiliary#OMEGA3.cci" "OMEGA3")
-let coq_OMEGA4 = lazy (constant "#auxiliary#OMEGA4.cci" "OMEGA4")
-let coq_OMEGA5 = lazy (constant "#auxiliary#OMEGA5.cci" "OMEGA5")
-let coq_OMEGA6 = lazy (constant "#auxiliary#OMEGA6.cci" "OMEGA6")
-let coq_OMEGA7 = lazy (constant "#auxiliary#OMEGA7.cci" "OMEGA7")
-let coq_OMEGA8 = lazy (constant "#auxiliary#OMEGA8.cci" "OMEGA8")
-let coq_OMEGA9 = lazy (constant "#auxiliary#OMEGA9.cci" "OMEGA9")
-let coq_fast_OMEGA10 = 
-  lazy (constant "#auxiliary#fast_OMEGA10.cci" "fast_OMEGA10")
-let coq_fast_OMEGA11 = 
-  lazy (constant "#auxiliary#fast_OMEGA11.cci" "fast_OMEGA11")
-let coq_fast_OMEGA12 = 
-  lazy (constant "#auxiliary#fast_OMEGA12.cci" "fast_OMEGA12")
-let coq_fast_OMEGA13 = 
-  lazy (constant "#auxiliary#fast_OMEGA13.cci" "fast_OMEGA13")
-let coq_fast_OMEGA14 = 
-  lazy (constant "#auxiliary#fast_OMEGA14.cci" "fast_OMEGA14")
-let coq_fast_OMEGA15 = 
-  lazy (constant "#auxiliary#fast_OMEGA15.cci" "fast_OMEGA15")
-let coq_fast_OMEGA16 = 
-  lazy (constant "#auxiliary#fast_OMEGA16.cci" "fast_OMEGA16")
-let coq_OMEGA17 = lazy (constant "#auxiliary#OMEGA17.cci" "OMEGA17")
-let coq_OMEGA18 = lazy (constant "#auxiliary#OMEGA18.cci" "OMEGA18")
-let coq_OMEGA19 = lazy (constant "#auxiliary#OMEGA19.cci" "OMEGA19")
-let coq_OMEGA20 = lazy (constant "#auxiliary#OMEGA20.cci" "OMEGA20")
-let coq_fast_Zred_factor0 = 
-  lazy (constant "#auxiliary#fast_Zred_factor0.cci" "fast_Zred_factor0")
-let coq_fast_Zred_factor1 = 
-  lazy (constant "#auxiliary#fast_Zred_factor1.cci" "fast_Zred_factor1")
-let coq_fast_Zred_factor2 = 
-  lazy (constant "#auxiliary#fast_Zred_factor2.cci" "fast_Zred_factor2")
-let coq_fast_Zred_factor3 = 
-  lazy (constant "#auxiliary#fast_Zred_factor3.cci" "fast_Zred_factor3")
-let coq_fast_Zred_factor4 = 
-  lazy (constant "#auxiliary#fast_Zred_factor4.cci" "fast_Zred_factor4")
-let coq_fast_Zred_factor5 = 
-  lazy (constant "#auxiliary#fast_Zred_factor5.cci" "fast_Zred_factor5")
-let coq_fast_Zred_factor6 = 
-  lazy (constant "#auxiliary#fast_Zred_factor6.cci" "fast_Zred_factor6")
+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_fast_Zmult_plus_distr =
-  lazy 
-    (constant "#auxiliary#fast_Zmult_plus_distr.cci" "fast_Zmult_plus_distr")
+  lazy (constant ["auxiliary"] "fast_Zmult_plus_distr")
 let coq_fast_Zmult_Zopp_left = 
-  lazy (constant "#auxiliary#fast_Zmult_Zopp_left.cci" "fast_Zmult_Zopp_left")
-let coq_fast_Zopp_Zplus = 
-  lazy (constant "#auxiliary#fast_Zopp_Zplus.cci" "fast_Zopp_Zplus")
-let coq_fast_Zopp_Zmult_r = 
-  lazy (constant "#auxiliary#fast_Zopp_Zmult_r.cci" "fast_Zopp_Zmult_r")
-let coq_fast_Zopp_one = 
-  lazy (constant "#auxiliary#fast_Zopp_one.cci" "fast_Zopp_one")
-let coq_fast_Zopp_Zopp = 
-  lazy (constant "#auxiliary#fast_Zopp_Zopp.cci" "fast_Zopp_Zopp")
-let coq_Zegal_left = lazy (constant "#auxiliary#Zegal_left.cci" "Zegal_left")
-let coq_Zne_left = lazy (constant "#auxiliary#Zne_left.cci" "Zne_left")
-let coq_Zlt_left = lazy (constant "#auxiliary#Zlt_left.cci" "Zlt_left")
-let coq_Zge_left = lazy (constant "#auxiliary#Zge_left.cci" "Zge_left")
-let coq_Zgt_left = lazy (constant "#auxiliary#Zgt_left.cci" "Zgt_left")
-let coq_Zle_left = lazy (constant "#auxiliary#Zle_left.cci" "Zle_left")
-let coq_eq_ind_r = lazy (constant "#auxiliary#eq_ind_r.cci" "eq_ind_r")
-let coq_new_var = lazy (constant "#auxiliary#new_var.cci" "new_var")
-let coq_intro_Z = lazy (constant "#auxiliary#intro_Z.cci" "intro_Z")
-let coq_dec_or = lazy (constant "#auxiliary#dec_or.cci" "dec_or")
-let coq_dec_and = lazy (constant "#auxiliary#dec_and.cci" "dec_and")
-let coq_dec_imp = lazy (constant "#auxiliary#dec_imp.cci" "dec_imp")
-let coq_dec_not = lazy (constant "#auxiliary#dec_not.cci" "dec_not")
-let coq_dec_eq_nat = lazy (constant "#auxiliary#dec_eq_nat.cci" "dec_eq_nat")
-let coq_dec_eq = lazy (constant "#auxiliary#dec_eq.cci" "dec_eq")
-let coq_dec_Zne = lazy (constant "#auxiliary#dec_Zne.cci" "dec_Zne")
-let coq_dec_Zle = lazy (constant "#auxiliary#dec_Zle.cci" "dec_Zle")
-let coq_dec_Zlt = lazy (constant "#auxiliary#dec_Zlt.cci" "dec_Zlt")
-let coq_dec_Zgt = lazy (constant "#auxiliary#dec_Zgt.cci" "dec_Zgt")
-let coq_dec_Zge = lazy (constant "#auxiliary#dec_Zge.cci" "dec_Zge")
-let coq_dec_le = lazy (constant "#auxiliary#dec_le.cci" "dec_le")
-let coq_dec_lt = lazy (constant "#auxiliary#dec_lt.cci" "dec_lt")
-let coq_dec_ge = lazy (constant "#auxiliary#dec_ge.cci" "dec_ge")
-let coq_dec_gt = lazy (constant "#auxiliary#dec_gt.cci" "dec_gt")
-let coq_dec_False = lazy (constant "#auxiliary#dec_False.cci" "dec_False")
-let coq_dec_not_not = 
-  lazy (constant "#auxiliary#dec_not_not.cci" "dec_not_not")
-let coq_dec_True = lazy (constant "#auxiliary#dec_True.cci" "dec_True")
-let coq_not_Zeq = lazy (constant "#auxiliary#not_Zeq.cci" "not_Zeq")
-let coq_not_Zle = lazy (constant "#auxiliary#not_Zle.cci" "not_Zle")
-let coq_not_Zlt = lazy (constant "#auxiliary#not_Zlt.cci" "not_Zlt")
-let coq_not_Zge = lazy (constant "#auxiliary#not_Zge.cci" "not_Zge")
-let coq_not_Zgt = lazy (constant "#auxiliary#not_Zgt.cci" "not_Zgt")
-let coq_not_le = lazy (constant "#auxiliary#not_le.cci" "not_le")
-let coq_not_lt = lazy (constant "#auxiliary#not_lt.cci" "not_lt")
-let coq_not_ge = lazy (constant "#auxiliary#not_ge.cci" "not_ge")
-let coq_not_gt = lazy (constant "#auxiliary#not_gt.cci" "not_gt")
-let coq_not_eq = lazy (constant "#auxiliary#not_eq.cci" "not_eq")
-let coq_not_or = lazy (constant "#auxiliary#not_or.cci" "not_or")
-let coq_not_and = lazy (constant "#auxiliary#not_and.cci" "not_and")
-let coq_not_imp = lazy (constant "#auxiliary#not_imp.cci" "not_imp")
-let coq_not_not = lazy (constant "#auxiliary#not_not.cci" "not_not")
-let coq_imp_simp = lazy (constant "#auxiliary#imp_simp.cci" "imp_simp")
-let coq_neq = lazy (constant "#auxiliary#neq.cci" "neq")
-let coq_Zne = lazy (constant "#auxiliary#Zne.cci" "Zne")
+  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")
 
 (* Compare_dec *)
-let coq_le_gt_dec = lazy (constant "#Compare_dec#le_gt_dec.cci" "le_gt_dec")
+let coq_le_gt_dec = lazy (constant ["Compare_dec"] "le_gt_dec")
 
 (* Peano *)
-let coq_le = lazy (constant "#Peano#le.cci" "le")
-let coq_gt = lazy (constant "#Peano#gt.cci" "gt")
+let coq_le = lazy (constant ["Peano"] "le")
+let coq_gt = lazy (constant ["Peano"] "gt")
 
 (* Datatypes *)
-let coq_nat = lazy (constant "#Datatypes#nat.cci" "nat")
-let coq_S = lazy (constant "#Datatypes#nat.cci" "S")
-let coq_O = lazy (constant "#Datatypes#nat.cci" "O")
+let coq_nat = lazy (constant ["Datatypes"] "nat")
+let coq_S = lazy (constant ["Datatypes"] "S")
+let coq_O = lazy (constant ["Datatypes"] "O")
 
 (* Minus *)
-let coq_minus = lazy (constant "#Minus#minus.cci" "minus")
+let coq_minus = lazy (constant ["Minus"] "minus")
 
 (* Logic *)
-let coq_eq = lazy (constant "#Logic#eq.cci" "eq")
-let coq_and = lazy (constant "#Logic#and.cci" "and")
-let coq_not = lazy (constant "#Logic#not.cci" "not")
-let coq_or = lazy (constant "#Logic#or.cci" "or")
-let coq_ex = lazy (constant "#Logic#ex.cci" "ex")
+let coq_eq = lazy (constant ["Logic"] "eq")
+let coq_and = lazy (constant ["Logic"] "and")
+let coq_not = lazy (constant ["Logic"] "not")
+let coq_or = lazy (constant ["Logic"] "or")
+let coq_ex = lazy (constant ["Logic"] "ex")
 
 (* Section paths for unfold *)
 let sp_Zs = path_of_string "#zarith_aux#Zs.cci"
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index a3dd19dd6..7aba0db66 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -113,8 +113,11 @@ open Proof_type
   the constants are loaded in the environment *)
 
 let constant sp id = 
+  Declare.global_qualified_reference
+    (make_path (dirpath (path_of_string sp)) (id_of_string id) CCI)
+(*
   Declare.global_sp_reference (path_of_string sp) (id_of_string id)
-
+*)
 let coq_Empty_vm = lazy (constant "#Quote#varmap.cci" "Empty_vm")
 let coq_Node_vm = lazy (constant "#Quote#varmap.cci" "Node_vm")
 let coq_varmap_find = lazy (constant "#Quote#varmap_find.cci" "varmap_find")
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 2a817668e..6080d7897 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -3,101 +3,91 @@
 
 (* ML part of the Ring tactic *)
 
-open Pp
-open Util
-open Term
-open Names
-open Reduction
-open Tacmach
-open Proof_type
-open Proof_trees
-open Printer
-open Equality
-open Vernacinterp
-open Libobject
-open Closure
-open Tacred
-open Tactics
-open Pattern 
-open Hiddentac
-open Quote
+open Pp;;
+open Util;;
+open Term;;
+open Names;;
+open Reduction;;
+open Tacmach;;
+open Proof_type;;
+open Proof_trees;;
+open Printer;;
+open Equality;;
+open Vernacinterp;;
+open Libobject;;
+open Closure;;
+open Tacred;;
+open Tactics;;
+open Pattern ;;
+open Hiddentac;;
+open Quote;;
 
 let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
-let constant sp id = 
-  Declare.global_sp_reference (path_of_string sp) (id_of_string id)
+let constant dir id = 
+  Declare.global_qualified_reference (make_path dir (id_of_string id) CCI)
 
 (* Ring_theory *)
 
-let coq_Ring_Theory = 
-  lazy (constant "#Ring_theory#Ring_Theory.cci" "Ring_Theory")
-let coq_Semi_Ring_Theory = 
-  lazy (constant "#Ring_theory#Semi_Ring_Theory.cci" "Semi_Ring_Theory")
+let coq_Ring_Theory = lazy (constant ["Ring_theory"] "Ring_Theory")
+let coq_Semi_Ring_Theory = lazy (constant ["Ring_theory"] "Semi_Ring_Theory")
 
 (* Ring_normalize *)
-let coq_SPplus = lazy (constant "#Ring_normalize#spolynomial.cci" "SPplus")
-let coq_SPmult = lazy (constant "#Ring_normalize#spolynomial.cci" "SPmult")
-let coq_SPvar = lazy (constant "#Ring_normalize#spolynomial.cci" "SPvar")
-let coq_SPconst = lazy (constant "#Ring_normalize#spolynomial.cci" "SPconst")
-let coq_Pplus = lazy (constant "#Ring_normalize#polynomial.cci" "Pplus")
-let coq_Pmult = lazy (constant "#Ring_normalize#polynomial.cci" "Pmult")
-let coq_Pvar = lazy (constant "#Ring_normalize#polynomial.cci" "Pvar")
-let coq_Pconst = lazy (constant "#Ring_normalize#polynomial.cci" "Pconst")
-let coq_Popp = lazy (constant "#Ring_normalize#polynomial.cci" "Popp")
-let coq_interp_sp = lazy (constant "#Ring_normalize#interp_sp.cci" "interp_sp")
-let coq_interp_p = lazy (constant "#Ring_normalize#interp_p.cci" "interp_p")
-let coq_interp_cs = lazy (constant "#Ring_normalize#interp_cs.cci" "interp_cs")
+let coq_SPplus = lazy (constant ["Ring_normalize"] "SPplus")
+let coq_SPmult = lazy (constant ["Ring_normalize"] "SPmult")
+let coq_SPvar = lazy (constant ["Ring_normalize"] "SPvar")
+let coq_SPconst = lazy (constant ["Ring_normalize"] "SPconst")
+let coq_Pplus = lazy (constant ["Ring_normalize"] "Pplus")
+let coq_Pmult = lazy (constant ["Ring_normalize"] "Pmult")
+let coq_Pvar = lazy (constant ["Ring_normalize"] "Pvar")
+let coq_Pconst = lazy (constant ["Ring_normalize"] "Pconst")
+let coq_Popp = lazy (constant ["Ring_normalize"] "Popp")
+let coq_interp_sp = lazy (constant ["Ring_normalize"] "interp_sp")
+let coq_interp_p = lazy (constant ["Ring_normalize"] "interp_p")
+let coq_interp_cs = lazy (constant ["Ring_normalize"] "interp_cs")
 let coq_spolynomial_simplify = 
-  lazy (constant "#Ring_normalize#spolynomial_simplify.cci" 
-	  "spolynomial_simplify")
+  lazy (constant ["Ring_normalize"] "spolynomial_simplify")
 let coq_polynomial_simplify = 
-  lazy (constant "#Ring_normalize#polynomial_simplify.cci"
-	  "polynomial_simplify")
+  lazy (constant ["Ring_normalize"] "polynomial_simplify")
 let coq_spolynomial_simplify_ok = 
-  lazy (constant "#Ring_normalize#spolynomial_simplify_ok.cci"
-	  "spolynomial_simplify_ok")
+  lazy (constant ["Ring_normalize"] "spolynomial_simplify_ok")
 let coq_polynomial_simplify_ok = 
-  lazy (constant "#Ring_normalize#polynomial_simplify_ok.cci"
-	  "polynomial_simplify_ok")
+  lazy (constant ["Ring_normalize"] "polynomial_simplify_ok")
 
 (* Ring_abstract *)
-let coq_ASPplus = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPplus")
-let coq_ASPmult = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPmult")
-let coq_ASPvar = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPvar")
-let coq_ASP0 = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASP0")
-let coq_ASP1 = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASP1")
-let coq_APplus = lazy (constant "#Ring_abstract#apolynomial.cci" "APplus")
-let coq_APmult = lazy (constant "#Ring_abstract#apolynomial.cci" "APmult")
-let coq_APvar = lazy (constant "#Ring_abstract#apolynomial.cci" "APvar")
-let coq_AP0 = lazy (constant "#Ring_abstract#apolynomial.cci" "AP0")
-let coq_AP1 = lazy (constant "#Ring_abstract#apolynomial.cci" "AP1")
-let coq_APopp = lazy (constant "#Ring_abstract#apolynomial.cci" "APopp")
+let coq_ASPplus = lazy (constant ["Ring_abstract"] "ASPplus")
+let coq_ASPmult = lazy (constant ["Ring_abstract"] "ASPmult")
+let coq_ASPvar = lazy (constant ["Ring_abstract"] "ASPvar")
+let coq_ASP0 = lazy (constant ["Ring_abstract"] "ASP0")
+let coq_ASP1 = lazy (constant ["Ring_abstract"] "ASP1")
+let coq_APplus = lazy (constant ["Ring_abstract"] "APplus")
+let coq_APmult = lazy (constant ["Ring_abstract"] "APmult")
+let coq_APvar = lazy (constant ["Ring_abstract"] "APvar")
+let coq_AP0 = lazy (constant ["Ring_abstract"] "AP0")
+let coq_AP1 = lazy (constant ["Ring_abstract"] "AP1")
+let coq_APopp = lazy (constant ["Ring_abstract"] "APopp")
 let coq_interp_asp = 
-  lazy (constant "#Ring_abstract#interp_asp.cci" "interp_asp")
+  lazy (constant ["Ring_abstract"] "interp_asp")
 let coq_interp_ap = 
-  lazy (constant "#Ring_abstract#interp_ap.cci" "interp_ap")
+  lazy (constant ["Ring_abstract"] "interp_ap")
  let coq_interp_acs = 
-  lazy (constant "#Ring_abstract#interp_acs.cci" "interp_acs")
+  lazy (constant ["Ring_abstract"] "interp_acs")
 let coq_interp_sacs = 
-  lazy (constant "#Ring_abstract#interp_sacs.cci" "interp_sacs")
+  lazy (constant ["Ring_abstract"] "interp_sacs")
 let coq_aspolynomial_normalize = 
-  lazy (constant "#Ring_abstract#aspolynomial_normalize.cci"
-	  "aspolynomial_normalize")
+  lazy (constant ["Ring_abstract"] "aspolynomial_normalize")
 let coq_apolynomial_normalize = 
-  lazy (constant "#Ring_abstract#apolynomial_normalize.cci"
-	  "apolynomial_normalize")
+  lazy (constant ["Ring_abstract"] "apolynomial_normalize")
 let coq_aspolynomial_normalize_ok = 
-  lazy (constant "#Ring_abstract#aspolynomial_normalize_ok.cci" 
-	  "aspolynomial_normalize_ok")
+  lazy (constant ["Ring_abstract"] "aspolynomial_normalize_ok")
 let coq_apolynomial_normalize_ok = 
-  lazy (constant "#Ring_abstract#apolynomial_normalize_ok.cci"
-	  "apolynomial_simplify_ok")
+  lazy (constant ["Ring_abstract"] "apolynomial_normalize_ok")
 
 (* Logic *)
-let coq_f_equal2 = lazy (constant "#Logic#f_equal2.cci" "f_equal2")
-let coq_eq = lazy (constant "#Logic#eq.cci" "eq")
-let coq_eqT = lazy (constant "#Logic_Type#eqT.cci" "eqT")
+let coq_f_equal2 = lazy (constant ["Logic"] "f_equal2")
+let coq_eq = lazy (constant ["Logic"] "eq")
+let coq_eqT = lazy (constant ["Logic_Type"] "eqT")
 
 (*********** Useful types and functions ************)