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

1 files changed, 162 insertions, 156 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 *)