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

12 files changed, 623 insertions, 539 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 518b98006a..fec7fb7018 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 81434acd16..b3421c9693 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 |]))))))
 
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
new file mode 100644
index 0000000000..94c23ef197
--- /dev/null
+++ b/parsing/coqlib.ml
@@ -0,0 +1,267 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Declare
+open Pattern
+
+let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI
+let myvar_path =
+  make_path ["Coq";"Arith";"Arith"] (id_of_string "My_special_variable") CCI
+
+let glob_nat = IndRef (nat_path,0)
+
+let glob_O = ConstructRef ((nat_path,0),1)
+let glob_S = ConstructRef ((nat_path,0),2)
+
+let glob_My_special_variable_nat = ConstRef myvar_path
+
+let reference dir s =
+  let dir = "Coq"::"Init"::[dir] in
+  try 
+    Nametab.locate_in_absolute_module dir (id_of_string s)
+  with Not_found ->
+    anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir s)))
+
+let constant dir s =
+  Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s)
+
+type coq_sigma_data = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  typ   : constr }
+
+type 'a delayed = unit -> 'a
+
+let build_sigma_set () =
+  { proj1 = constant "Specif" "projS1";
+    proj2 = constant "Specif" "projS2";
+    elim = constant "Specif" "sigS_rec";
+    intro = constant "Specif" "existS";
+    typ = constant "Specif" "sigS" }
+
+let build_sigma_type () =
+  { proj1 = constant "Logic_Type" "projT1";
+    proj2 = constant "Logic_Type" "projT2";
+    elim = constant "Logic_Type" "sigT_rec";
+    intro = constant "Logic_Type" "existT";
+    typ = constant "Logic_Type" "sigT" }
+
+(* Equalities *)
+type coq_leibniz_eq_data = {
+  eq   : constr delayed;
+  ind  : constr delayed;
+  rrec : constr delayed option;
+  rect : constr delayed option;
+  congr: constr delayed;
+  sym  : constr delayed }
+
+let constant dir id = lazy (constant dir id)
+
+(* Equality on Set *)
+let coq_eq_eq = constant "Logic" "eq"
+let coq_eq_ind = constant "Logic" "eq_ind"
+let coq_eq_rec = constant "Logic" "eq_rec"
+let coq_eq_rect = constant "Logic" "eq_rect"
+let coq_eq_congr = constant "Logic" "f_equal"
+let coq_eq_sym  = constant "Logic" "sym_eq"
+let coq_f_equal2 = constant "Logic" "f_equal2"
+
+let build_coq_eq_data = {
+  eq = (fun () -> Lazy.force coq_eq_eq);
+  ind = (fun () -> Lazy.force coq_eq_ind);
+  rrec = Some (fun () -> Lazy.force coq_eq_rec);
+  rect = Some (fun () -> Lazy.force coq_eq_rect);
+  congr = (fun () -> Lazy.force coq_eq_congr);
+  sym  = (fun () -> Lazy.force coq_eq_sym) }
+
+let build_coq_eq = build_coq_eq_data.eq
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+(* Specif *)
+let coq_sumbool  = constant "Specif" "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type *)
+let coq_eqT_eq = constant "Logic_Type" "eqT"
+let coq_eqT_ind = constant "Logic_Type" "eqT_ind"
+let coq_eqT_congr =constant "Logic_Type" "congr_eqT"
+let coq_eqT_sym  = constant "Logic_Type" "sym_eqT"
+
+let build_coq_eqT_data = {
+  eq = (fun () -> Lazy.force coq_eqT_eq);
+  ind = (fun () -> Lazy.force coq_eqT_ind);
+  rrec = None;
+  rect = None;
+  congr = (fun () -> Lazy.force coq_eqT_congr);
+  sym  = (fun () -> Lazy.force coq_eqT_sym) }
+
+let build_coq_eqT = build_coq_eqT_data.eq
+let build_coq_sym_eqT = build_coq_eqT_data.sym
+
+(* Equality on Type as a Type *)
+let coq_idT_eq = constant "Logic_Type" "identityT"
+let coq_idT_ind = constant "Logic_Type" "identityT_ind"
+let coq_idT_rec = constant "Logic_Type" "identityT_rec"
+let coq_idT_rect = constant "Logic_Type" "identityT_rect"
+let coq_idT_congr = constant "Logic_Type" "congr_idT"
+let coq_idT_sym = constant "Logic_Type" "sym_idT"
+
+let build_coq_idT_data = {
+  eq = (fun () -> Lazy.force coq_idT_eq);
+  ind = (fun () -> Lazy.force coq_idT_ind);
+  rrec = Some (fun () -> Lazy.force coq_idT_rec);
+  rect = Some (fun () -> Lazy.force coq_idT_rect);
+  congr = (fun () -> Lazy.force coq_idT_congr);
+  sym  = (fun () -> Lazy.force coq_idT_sym) }
+
+(* Empty Type *)
+let coq_EmptyT = constant "Logic_Type" "EmptyT"
+
+(* Unit Type and its unique inhabitant *)
+let coq_UnitT  = constant "Logic_Type" "UnitT"
+let coq_IT     = constant "Logic_Type" "IT"
+
+(* The False proposition *)
+let coq_False  = constant "Logic" "False"
+
+(* The True proposition and its unique proof *)
+let coq_True   = constant "Logic" "True"
+let coq_I      = constant "Logic" "I"
+
+(* Connectives *)
+let coq_not = constant "Logic" "not"
+let coq_and = constant "Logic" "and"
+let coq_or = constant "Logic" "or"
+let coq_ex = constant "Logic" "ex"
+
+(* Runtime part *)
+let build_coq_EmptyT () = Lazy.force coq_EmptyT
+let build_coq_UnitT () = Lazy.force coq_UnitT
+let build_coq_IT ()    = Lazy.force coq_IT
+
+let build_coq_True ()  = Lazy.force coq_True
+let build_coq_I ()     = Lazy.force coq_I
+
+let build_coq_False () = Lazy.force coq_False
+let build_coq_not ()   = Lazy.force coq_not
+let build_coq_and ()   = Lazy.force coq_and
+let build_coq_or ()   = Lazy.force coq_or
+let build_coq_ex ()   = Lazy.force coq_ex
+
+(****************************************************************************)
+(*                             Patterns                                     *)
+(* This needs to have interp_constrpattern available ...
+let parse_astconstr s =
+  try 
+    Pcoq.parse_string Pcoq.Constr.constr_eoi s 
+  with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
+    error "Syntax error : not a construction"
+
+let parse_pattern s =
+  Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s)
+
+let coq_eq_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
+let coq_eqT_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.eqT ?1 ?2 ?3)"))
+let coq_idT_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)"))
+let coq_existS_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)"))
+let coq_existT_pattern = 
+  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.existT ?1 ?2 ?3 ?4)"))
+let coq_not_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic.not ?)"))
+let coq_imp_False_pattern =
+  lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_imp_False_pattern =
+  lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_eqdec_partial_pattern
+  lazy (snd (parse_pattern "(sumbool (eq ?1 ?2 ?3) ?4)"))
+let coq_eqdec_pattern
+  lazy (snd (parse_pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
+*)
+
+(* The following is less readable but does not depend on parsing *)
+let coq_eq_ref      = lazy (reference "Logic" "eq")
+let coq_eqT_ref     = lazy (reference "Logic_Type" "eqT")
+let coq_idT_ref     = lazy (reference "Logic_Type" "identityT")
+let coq_existS_ref  = lazy (reference "Specif" "existS")
+let coq_existT_ref  = lazy (reference "Logic_Type" "existT")
+let coq_not_ref     = lazy (reference "Logic" "not")
+let coq_False_ref   = lazy (reference "Logic" "False")
+let coq_sumbool_ref = lazy (reference "Specif" "sumbool")
+
+(* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *)
+let coq_eq_pattern_gen eq = 
+  lazy (PApp(PRef (Lazy.force eq), Array.init 3 (fun i -> PMeta (Some (i+1)))))
+let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
+let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref
+let coq_idT_pattern = coq_eq_pattern_gen coq_idT_ref
+
+(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
+let coq_ex_pattern_gen ex =
+  lazy (PApp(PRef (Lazy.force ex), Array.init 4 (fun i -> PMeta (Some (i+1)))))
+let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref
+let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
+
+(* Patterns "~ ?", "? -> False" and "(?1 -> ?2)" *)
+let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|]))
+let imp a b = PProd (Anonymous, a, b)
+let coq_imp_False_pattern =
+  lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref)))
+let coq_arrow_pattern = lazy (imp (PMeta (Some 1)) (PMeta (Some 2)))
+
+(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *)
+let coq_eqdec_partial_pattern =
+  lazy
+    (PApp
+       (PRef (Lazy.force coq_sumbool_ref),
+	[| Lazy.force coq_eq_pattern; PMeta (Some 4) |]))
+
+(* The expected form of the goal for the tactic Decide Equality *)
+
+(* Pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" *)
+(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *)
+let x = Name (id_of_string "x")
+let y = Name (id_of_string "y")
+let coq_eqdec_pattern =
+  lazy
+    (PProd (x, PMeta (Some 1), PProd (y, PMeta (Some 1), 
+    PApp (PRef (Lazy.force coq_sumbool_ref),
+	  [| PApp (PRef (Lazy.force coq_eq_ref),
+		   [| PMeta (Some 1); PRel 2; PRel 1 |]);
+	     PApp (PRef (Lazy.force coq_not_ref), 
+		   [|PApp (PRef (Lazy.force coq_eq_ref),
+ 			   [| PMeta (Some 1); PRel 2; PRel 1 |])|]) |]))))
+
+(* "(A : ?)(x:A)(? A x x)" and "(x : ?)(? x x)" *)
+let name_A = Name (id_of_string "A")
+let coq_refl_rel1_pattern =
+  lazy
+    (PProd
+       (name_A, PMeta None,
+	PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|]))))
+let coq_refl_rel2_pattern =
+  lazy
+    (PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|])))
+
+
+let build_coq_eq_pattern () = Lazy.force coq_eq_pattern
+let build_coq_eqT_pattern () = Lazy.force coq_eqT_pattern
+let build_coq_idT_pattern () = Lazy.force coq_idT_pattern
+let build_coq_existS_pattern () = Lazy.force coq_existS_pattern
+let build_coq_existT_pattern () = Lazy.force coq_existT_pattern
+let build_coq_not_pattern () = Lazy.force coq_not_pattern
+let build_coq_imp_False_pattern () = Lazy.force coq_imp_False_pattern
+let build_coq_eqdec_partial_pattern () = Lazy.force coq_eqdec_partial_pattern
+let build_coq_eqdec_pattern () = Lazy.force coq_eqdec_pattern
+let build_coq_arrow_pattern () = Lazy.force coq_arrow_pattern
+let build_coq_refl_rel1_pattern () = Lazy.force coq_refl_rel1_pattern
+let build_coq_refl_rel2_pattern () = Lazy.force coq_refl_rel2_pattern
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli
new file mode 100644
index 0000000000..c835eeffa3
--- /dev/null
+++ b/parsing/coqlib.mli
@@ -0,0 +1,113 @@
+
+(* $Id$ *)
+
+(*i*)
+open Term
+open Pattern
+(*i*)
+
+(*s This module collects the global references of the standard library
+    used in ocaml files *)
+
+(* Natural numbers *)
+val glob_nat : global_reference
+val glob_O : global_reference
+val glob_S : global_reference
+
+(* Special variable for pretty-printing of constant naturals *)
+val glob_My_special_variable_nat : global_reference
+
+(*s For Equality tactics *)
+type coq_sigma_data = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  typ   : constr }
+
+val build_sigma_set : unit -> coq_sigma_data
+val build_sigma_type : unit -> coq_sigma_data
+
+type 'a delayed = unit -> 'a
+
+type coq_leibniz_eq_data = {
+  eq   : constr delayed;
+  ind  : constr delayed;
+  rrec : constr delayed option;
+  rect : constr delayed option;
+  congr: constr delayed;
+  sym  : constr delayed }
+
+val build_coq_eq_data : coq_leibniz_eq_data
+val build_coq_eqT_data : coq_leibniz_eq_data
+val build_coq_idT_data : coq_leibniz_eq_data
+
+val build_coq_f_equal2 : constr delayed
+val build_coq_eqT : constr delayed
+val build_coq_sym_eqT : constr delayed
+
+(* Empty Type *)
+val build_coq_EmptyT : constr delayed
+
+(* Unit Type and its unique inhabitant *)
+val build_coq_UnitT : constr delayed
+val build_coq_IT : constr delayed
+
+(* Specif *)
+val build_coq_sumbool : constr delayed
+
+(*s Connectives *)
+(* The False proposition *)
+val build_coq_False : constr delayed
+
+(* The True proposition and its unique proof *)
+val build_coq_True : constr delayed
+val build_coq_I : constr delayed
+
+(* Negation *)
+val build_coq_not : constr delayed
+
+(* Conjunction *)
+val build_coq_and : constr delayed
+
+(* Disjunction *)
+val build_coq_or : constr delayed
+
+(* Existential quantifier *)
+val build_coq_ex : constr delayed
+
+(**************************** Patterns ************************************)
+(* ["(eq ?1 ?2 ?3)"] *)
+val build_coq_eq_pattern : constr_pattern delayed
+
+(* ["(eqT ?1 ?2 ?3)"] *)
+val build_coq_eqT_pattern : constr_pattern delayed
+
+(* ["(identityT ?1 ?2 ?3)"] *)
+val build_coq_idT_pattern : constr_pattern delayed
+
+(* ["(existS ?1 ?2 ?3 ?4)"] *)
+val build_coq_existS_pattern : constr_pattern delayed
+
+(* ["(existT ?1 ?2 ?3 ?4)"] *)
+val build_coq_existT_pattern : constr_pattern delayed
+
+(* ["(not ?)"] *)
+val build_coq_not_pattern : constr_pattern delayed
+
+(* ["? -> False"] *)
+val build_coq_imp_False_pattern : constr_pattern delayed
+
+(* ["(sumbool (eq ?1 ?2 ?3) ?4)"] *)
+val build_coq_eqdec_partial_pattern : constr_pattern delayed
+
+(* ["! (x,y:?1). (sumbool (eq ?1 x y) ~(eq ?1 x y))"] *)
+val build_coq_eqdec_pattern : constr_pattern delayed
+
+(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *)
+val build_coq_refl_rel1_pattern : constr_pattern delayed
+val build_coq_refl_rel2_pattern : constr_pattern delayed
+
+(* ["(?1 -> ?2)"] *)
+val build_coq_arrow_pattern : constr_pattern delayed
+
diff --git a/parsing/stdlib.ml b/parsing/stdlib.ml
deleted file mode 100644
index 8c4e2bf681..0000000000
--- a/parsing/stdlib.ml
+++ /dev/null
@@ -1,17 +0,0 @@
-
-(* $Id$ *)
-
-open Names
-open Term
-open Declare
-
-let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI
-let myvar_path =
-  make_path ["Coq";"Arith";"Arith"] (id_of_string "My_special_variable") CCI
-
-let glob_nat = IndRef (nat_path,0)
-
-let glob_O = ConstructRef ((nat_path,0),1)
-let glob_S = ConstructRef ((nat_path,0),2)
-
-let glob_My_special_variable_nat = ConstRef myvar_path
diff --git a/parsing/stdlib.mli b/parsing/stdlib.mli
deleted file mode 100644
index 7bb890d18d..0000000000
--- a/parsing/stdlib.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-
-(* $Id$ *)
-
-open Term
-
-(*s This module collects the global references of the standard library
-    used in ocaml files *)
-
-(* Natural numbers *)
-val glob_nat : global_reference
-val glob_O : global_reference
-val glob_S : global_reference
-
-(* Special variable for pretty-printing of constant naturals *)
-val glob_My_special_variable_nat : global_reference
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 728430f065..1897a8ba6f 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -14,6 +14,7 @@ open Hipattern
 open Proof_trees
 open Proof_type
 open Tacmach
+open Coqlib
 
 (* This file containts the implementation of the tactics ``Decide
    Equality'' and ``Compare''. They can be used to decide the
@@ -56,15 +57,10 @@ let h_solveRightBranch =
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
-let mmk         = make_module_marker [ "Logic"; "Specif" ]
-let eqpat       = put_squel mmk "eq"                 
-let sumboolpat  = put_squel mmk "sumbool"             
-let notpat      = put_squel mmk "not"   
-
 let mkDecideEqGoal rectype c1 c2 g = 
-  let equality    = mkAppA [|get_squel eqpat;rectype;c1;c2|] in
-  let disequality = mkAppA [|get_squel notpat;equality|] in
-  mkAppA [|get_squel sumboolpat;equality;disequality |]
+  let equality    = mkAppA [|build_coq_eq_data.eq (); rectype; c1; c2|] in
+  let disequality = mkAppA [|build_coq_not (); equality|] in
+  mkAppA [|build_coq_sumbool (); equality; disequality |]
 
 
 (* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
@@ -101,11 +97,9 @@ let solveArg a1 a2 tac  g =
      (h_elimType decide) 
      [(eqCase tac);diseqCase;default_auto]) g
 
-let conclpatt = lazy (get_pat (put_pat mmk "{<?1>?2=?3}+{?4}"))
-
 let solveLeftBranch rectype g =
   match
-    try matches (Lazy.force conclpatt) (pf_concl g)
+    try matches (Coqlib.build_coq_eqdec_partial_pattern ()) (pf_concl g)
     with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!"
   with 
     | _ :: lhs :: rhs :: _ -> 
@@ -118,10 +112,6 @@ let solveLeftBranch rectype g =
     | _ -> anomaly "Unexpected pattern for solveLeftBranch"
 
 
-(* The expected form of the goal for the tactic Decide Equality *)
-
-let initialpatt = lazy (get_pat (put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
-
 (* The tactic Decide Equality *)
 
 let hd_app c = match kind_of_term c with
@@ -130,7 +120,7 @@ let hd_app c = match kind_of_term c with
 
 let decideGralEquality g =
   match
-    try matches (Lazy.force initialpatt) (pf_concl g)
+    try matches (build_coq_eqdec_pattern ()) (pf_concl g)
     with Pattern.PatternMatchingFailure ->
       error "The goal does not have the expected form"
   with 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9b31819279..726131deea 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -24,6 +24,7 @@ open Tactics
 open Tacinterp
 open Tacred
 open Vernacinterp
+open Coqlib
 
 (* Rewriting tactics *)
 
@@ -44,14 +45,12 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
     | None -> error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_head hdcncl in 
+	let suffix = Declare.elimination_suffix (sort_of_goal gl) in
         let elim =
 	  if lft2rgt then
-            pf_global gl
-	      (id_of_string 
-		 (hdcncls^(Declare.elimination_suffix (sort_of_goal gl))^"_r"))
+            pf_global gl (id_of_string (hdcncls^suffix^"_r"))
           else
-	    pf_global gl
-	      (id_of_string (hdcncls^(Declare.elimination_suffix (sort_of_goal gl))))
+	    pf_global gl (id_of_string (hdcncls^suffix))
         in 
 	tclNOTSAMEGOAL (general_elim (c,l) (elim,[])) gl
    (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
@@ -176,91 +175,17 @@ let find_constructor env sigma c =
     | IsMutConstruct _ -> (hd,stack)
     | _ -> error "find_constructor"
 
-type leibniz_eq = {
-  eq   : marked_term;
-  ind  : marked_term;
-  rrec : marked_term option;
-  rect : marked_term option;
-  congr: marked_term;
-  sym  : marked_term }
-
-type sigma_type = {
-  proj1 : constr;
-  proj2 : constr;
-  elim  : constr;
-  intro : constr;
-  typ   : constr }
-
-let mmk = make_module_marker [ "Prelude"; "Logic_Type"; "Specif"; "Logic" ]
-
 (* Patterns *)
-let eq_pattern_mark = put_pat mmk "(eq ?1 ?2 ?3)"
-let not_pattern_mark = put_pat mmk "(not ?)"
-let imp_False_pattern_mark = put_pat mmk "? -> False"
-
-let eq_pattern () = get_pat eq_pattern_mark
-let not_pattern () = get_pat not_pattern_mark
-let imp_False_pattern () = get_pat imp_False_pattern_mark
-
-let eq = { eq = put_squel mmk "eq";
-           ind = put_squel mmk "eq_ind" ;
-           rrec = Some (put_squel mmk "eq_rec");
-           rect = Some (put_squel mmk "eq_rect");
-           congr = put_squel mmk "f_equal"  ;
-           sym  = put_squel mmk "sym_eq" }
-
-let build_eq eq = get_squel eq.eq
-let build_ind eq = get_squel eq.ind
+
+let build_coq_eq eq = eq.eq ()
+let build_ind eq = eq.ind ()
 let build_rect eq = 
   match eq.rect with
     | None -> assert false
-    | Some sq -> get_squel sq
+    | Some c -> c ()
 	  
-let eqT_pattern_mark = put_pat mmk "(eqT ?1 ?2 ?3)"
-let eqT_pattern () = get_pat eqT_pattern_mark
- 
-let eqT = { eq  = put_squel mmk "eqT";
-            ind = put_squel mmk "eqT_ind" ;
-            rrec = None;
-            rect = None;
-            congr = put_squel mmk "congr_eqT"  ;
-            sym  = put_squel mmk "sym_eqT" }
-
-let idT_pattern_mark = put_pat mmk "(identityT ?1 ?2 ?3)"
-let idT_pattern () = get_pat idT_pattern_mark
-
-let idT = { eq  = put_squel mmk "identityT";
-            ind = put_squel mmk "identityT_ind" ;
-            rrec = Some (put_squel mmk "identityT_rec")  ;
-            rect = Some (put_squel mmk "identityT_rect");
-            congr = put_squel mmk "congr_idT"  ;
-            sym  = put_squel mmk "sym_idT" }
-
 (* List of constructions depending of the initial state *)
 
-(* Initialisation part *)
-let squel_EmptyT = put_squel mmk "EmptyT"
-let squel_True   = put_squel mmk "True"
-let squel_False  = put_squel mmk "False"
-let squel_UnitT  = put_squel mmk "UnitT"
-let squel_IT     = put_squel mmk "IT"
-let squel_I      = put_squel mmk "I"
-
-(* Runtime part *)
-let build_EmptyT () = get_squel squel_EmptyT
-let build_True ()  = get_squel squel_True
-let build_False () = get_squel squel_False
-let build_UnitT () = get_squel squel_UnitT
-let build_IT ()    = get_squel squel_IT
-let build_I ()     = get_squel squel_I
-
-let pat_False_mark  = put_pat mmk "False"
-let pat_False () = get_pat pat_False_mark
-let pat_EmptyT_mark = put_pat mmk "EmptyT"
-let pat_EmptyT () = get_pat pat_EmptyT_mark
-
-let notT_pattern = put_pat mmk "(notT ?)"
-
 (* Destructuring patterns *)
 let match_eq eqn eq_pat =
   match matches eqn eq_pat with
@@ -294,14 +219,11 @@ let necessary_elimination sort_arity sort =
         [< 'sTR "no primitive equality on proofs" >]
 
 let find_eq_pattern aritysort sort = 
-  let mt =
-    match necessary_elimination aritysort sort with
-      | Set_Type       ->  eq.eq
-      | Type_Type      ->  idT.eq
-      | Set_SetorProp  ->  eq.eq
-      | Type_SetorProp ->  eqT.eq
-  in 
-  get_squel mt
+  match necessary_elimination aritysort sort with
+    | Set_Type       ->  build_coq_eq_data.eq ()
+    | Type_Type      ->  build_coq_idT_data.eq ()
+    | Set_SetorProp  ->  build_coq_eq_data.eq ()
+    | Type_SetorProp ->  build_coq_eqT_data.eq ()
 
 (* [find_positions t1 t2]
 
@@ -501,8 +423,8 @@ let construct_discriminator sigma env dirn c sort =
   let arsign,arsort = get_arity indf in
   let (true_0,false_0,sort_0) = 
     match necessary_elimination arsort (destSort sort) with
-      | Type_Type -> build_UnitT (), build_EmptyT (), (Type dummy_univ)
-      | _         -> build_True (),  build_False (),  (Prop Null)
+      | Type_Type -> build_coq_UnitT (), build_coq_EmptyT (), (Type dummy_univ)
+      | _         -> build_coq_True (),  build_coq_False (),  (Prop Null)
   in
   let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in
   let cstrs = get_constructors indf in
@@ -529,22 +451,25 @@ let rec build_discriminator sigma env dirn c sort = function
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       (match necessary_elimination arsort (destSort sort) with
          | Type_Type ->
-	     kont subval (build_EmptyT (),mkSort (Type(dummy_univ)))
-	 | _ -> kont subval (build_False (),mkSort (Prop Null)))
+	     kont subval (build_coq_EmptyT (),mkSort (Type(dummy_univ)))
+	 | _ -> kont subval (build_coq_False (),mkSort (Prop Null)))
 
 let find_eq_data_decompose eqn =
-  if (is_matching (eq_pattern ()) eqn) then
-    (eq, match_eq (eq_pattern ()) eqn)
-  else if (is_matching (eqT_pattern ()) eqn) then
-    (eqT, match_eq (eqT_pattern ()) eqn)
-  else if (is_matching (idT_pattern ()) eqn) then
-    (idT, match_eq (idT_pattern ()) eqn)
+  if (is_matching (build_coq_eq_pattern ()) eqn) then
+    (build_coq_eq_data, match_eq (build_coq_eq_pattern ()) eqn)
+  else if (is_matching (build_coq_eqT_pattern ()) eqn) then
+    (build_coq_eqT_data, match_eq (build_coq_eqT_pattern ()) eqn)
+  else if (is_matching (build_coq_idT_pattern ()) eqn) then
+    (build_coq_idT_data, match_eq (build_coq_idT_pattern ()) eqn)
   else
     errorlabstrm  "find_eq_data_decompose" [< >]
 
 let gen_absurdity id gl =
+(*
   if   (pf_is_matching gl (pat_False ()) (clause_type (Some id) gl)) 
     or (pf_is_matching gl (pat_EmptyT ()) (clause_type  (Some id) gl))
+*)
+  if is_empty_type (clause_type (Some id) gl)
   then
     simplest_elim (mkVar id) gl
   else
@@ -565,14 +490,14 @@ let gen_absurdity id gl =
 let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
   let env = pf_env gls in
   let (indt,_) = find_mrectype env (project gls) t in 
-  let arity = Global.mind_nf_arity indt in
+  let aritysort = mis_sort (Global.lookup_mind_specif indt) in
   let sort = pf_type_of gls (pf_concl gls) in
-  match necessary_elimination (snd (destArity arity)) (destSort sort) with
+  match necessary_elimination aritysort (destSort sort) with
     | Type_Type  ->
  	let eq_elim     = build_rect lbeq in
-	let eq_term     = build_eq lbeq in
-	let i           = build_IT () in
-	let absurd_term = build_EmptyT () in
+	let eq_term     = build_coq_eq lbeq in
+	let i           = build_coq_IT () in
+	let absurd_term = build_coq_EmptyT () in
         let h = pf_get_new_id (id_of_string "HH")gls in
         let pred= mkNamedLambda e t 
                     (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) 
@@ -580,8 +505,8 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
         in (applist(eq_elim, [t;t1;pred;i;t2]), absurd_term)
 	     
     | _ ->
-	let i           = build_I () in
-	let absurd_term = build_False ()
+	let i           = build_coq_I () in
+	let absurd_term = build_coq_False ()
 
  in
 	let eq_elim     = build_ind lbeq in
@@ -610,7 +535,6 @@ let discr id gls =
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (indt,_) = find_mrectype env sigma t in 
-	 let arity = Global.mind_nf_arity indt in
 	 let (pf, absurd_term) =
 	   discrimination_pf e (t,t1,t2) discriminator lbeq gls 
 	 in
@@ -637,9 +561,9 @@ let discrOnLastHyp gls =
 let discrClause cls gls =
   match cls with
     | None ->
-    	if is_matching (not_pattern ()) (pf_concl gls) then
+    	if is_matching (build_coq_not_pattern ()) (pf_concl gls) then
           (tclTHEN (tclTHEN hnf_in_concl intro) discrOnLastHyp) gls
-    	else if is_matching (imp_False_pattern ()) (pf_concl gls)  then
+    	else if is_matching (build_coq_imp_False_pattern ()) (pf_concl gls)then
 	  (tclTHEN intro discrOnLastHyp) gls
 	else 
 	  errorlabstrm "DiscrClause" (insatisfied_prec_message cls)
@@ -666,27 +590,6 @@ let h_discrConcl = hide_atomic_tactic "DiscrConcl" discrConcl
 let h_discrHyp   = hide_ident_tactic  "DiscrHyp"   discrHyp
 (**)
 
-let existS_pattern = put_pat mmk "(existS ?1 ?2 ?3 ?4)"
-let existT_pattern = put_pat mmk "(existT ?1 ?2 ?3 ?4)"
-
-let constant dir s =
-  Declare.global_absolute_reference
-    (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI)
-
-let build_sigma_set () =
-  { proj1 = constant ["Specif"] "projS1";
-    proj2 = constant ["Specif"] "projS2";
-    elim = constant ["Specif"] "sigS_rec";
-    intro = constant ["Specif"] "existS";
-    typ = constant ["Specif"] "sigS" }
-
-let build_sigma_type () =
-  { proj1 = constant ["Specif"] "projT1";
-    proj2 = constant ["Specif"] "projT2";
-    elim = constant ["Specif"] "sigT_rec";
-    intro = constant ["Specif"] "existT";
-    typ = constant ["Specif"] "sigT" }
-
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
 
@@ -907,7 +810,7 @@ let inj id gls =
 	    [<'sTR "Failed to decompose the equality">];
 	tclMAP 
 	  (fun (injfun,resty) ->
-	     let pf = applist(get_squel eq.congr,
+	     let pf = applist(eq.congr (),
 			      [t;resty;injfun;
 			       try_delta_expand env sigma t1;
 			       try_delta_expand env sigma t2;
@@ -921,7 +824,7 @@ let inj id gls =
 let injClause cls gls =
   match cls with
     | None ->
-    	if is_matching (not_pattern ()) (pf_concl gls) then
+    	if is_matching (build_coq_not_pattern ()) (pf_concl gls) then
           (tclTHEN (tclTHEN hnf_in_concl intro)
              (onLastHyp (compose inj out_some))) gls
     	else
@@ -930,8 +833,6 @@ let injClause cls gls =
 	try 
 	  inj id gls
         with
-	  | Not_found ->
-	      errorlabstrm "InjClause" (not_found_message id)
           | UserError("refiner__fail",_) -> 
               errorlabstrm "InjClause" 
 		[< 'sTR (string_of_id id); 'sTR" Not a projectable equality" >]
@@ -984,7 +885,7 @@ let decompEqThen ntac id gls =
               [<'sTR "Discriminate failed to decompose the equality">];
 	  ((tclTHEN
 	      (tclMAP (fun (injfun,resty) ->
-			 let pf = applist(get_squel lbeq.congr,
+			 let pf = applist(lbeq.congr (),
 					  [t;resty;injfun;t1;t2;
 					   mkVar id]) in
 			 let ty = pf_type_of gls pf in
@@ -999,7 +900,7 @@ let decompEq = decompEqThen (fun x -> tclIDTAC)
 let dEqThen ntac cls gls =
   match cls with
     | None ->
-    	if is_matching (not_pattern ()) (pf_concl gls) then
+    	if is_matching (build_coq_not_pattern ()) (pf_concl gls) then
 	  (tclTHEN hnf_in_concl
 	     (tclTHEN intro
          	(onLastHyp (compose (decompEqThen ntac) out_some)))) gls
@@ -1036,7 +937,7 @@ let swap_equands gls eqn =
       find_eq_data_decompose eqn
     with _ -> errorlabstrm "swap_equamds" (rewrite_msg None)
   in 
-  applist(get_squel lbeq.eq,[t;e2;e1])
+  applist(lbeq.eq (),[t;e2;e1])
 
 let swapEquandsInConcl gls =
   let (lbeq,(t,e1,e2)) =
@@ -1044,7 +945,7 @@ let swapEquandsInConcl gls =
       find_eq_data_decompose (pf_concl gls)
     with _-> errorlabstrm "SwapEquandsInConcl" (rewrite_msg None) 
   in
-  let sym_equal = get_squel lbeq.sym in
+  let sym_equal = lbeq.sym () in
   refine (applist(sym_equal,[t;e2;e1;mkMeta (new_meta())])) gls
 
 let swapEquandsInHyp id gls =
@@ -1059,15 +960,15 @@ let swapEquandsInHyp id gls =
 
 let find_elim  sort_of_gl  lbeq =
   match kind_of_term sort_of_gl  with
-    | IsSort(Prop Null)  (* Prop *)  ->  (get_squel lbeq.ind, false)  
+    | IsSort(Prop Null)  (* Prop *)  ->  (lbeq.ind (), false)  
     | IsSort(Prop Pos)   (* Set *)   ->  
 	(match lbeq.rrec with
-           | Some eq_rec -> (get_squel eq_rec, false) 
+           | Some eq_rec -> (eq_rec (), false) 
 	   | None -> errorlabstrm "find_elim"
 		 [< 'sTR "this type of elimination is not allowed">])
     | _ (* Type *) -> 
         (match lbeq.rect with
-           | Some eq_rect -> (get_squel eq_rect, true) 
+           | Some eq_rect -> (eq_rect (), true) 
            | None -> errorlabstrm "find_elim"
 		 [< 'sTR "this type of elimination is not allowed">])
 
@@ -1078,7 +979,7 @@ let find_elim  sort_of_gl  lbeq =
 let build_dependent_rewrite_predicate (t,t1,t2) body lbeq gls =
   let e = pf_get_new_id  (id_of_string "e") gls in 
   let h = pf_get_new_id  (id_of_string "HH") gls in 
-  let eq_term = get_squel lbeq.eq in
+  let eq_term = lbeq.eq () in
   (mkNamedLambda e t 
      (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) 
         (lift 1 body))) 
@@ -1135,18 +1036,18 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
  *)
 
 let match_sigma ex ex_pat =
-  match matches (get_pat ex_pat) ex with
+  match matches ex_pat ex with
     | [(1,a);(2,p);(3,car);(4,cdr)] -> (a,p,car,cdr)
     | _ ->
 	anomaly "match_sigma: a successful sigma pattern should match 4 terms"
 
 let find_sigma_data_decompose ex =
   try
-    let subst = match_sigma ex existS_pattern in
+    let subst = match_sigma ex (build_coq_existS_pattern ()) in
     (build_sigma_set (),subst)
   with PatternMatchingFailure ->
     (try 
-       let subst = match_sigma ex existT_pattern in
+       let subst = match_sigma ex (build_coq_existT_pattern ()) in
        (build_sigma_type (),subst)
      with PatternMatchingFailure -> 
        errorlabstrm "find_sigma_data_decompose" [< >])
@@ -1352,7 +1253,7 @@ let sub_term_with_unif cref ceq =
 let general_rewrite_in lft2rgt id (c,lb) gls =
   let typ_id =
     (try
-       let (_,ty) = lookup_named id (pf_env gls) in (body_of_type ty)
+       let (_,ty) = lookup_named id (pf_env gls) in ty
      with Not_found -> 
        errorlabstrm "general_rewrite_in" 
 	 [< 'sTR"No such hypothesis : "; pr_id id >])
@@ -1375,10 +1276,10 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
            | None ->
                errorlabstrm "general_rewrite_in" 
 		 [<'sTR "Nothing to rewrite in: "; pr_id id>]
-           |Some (l2,nb_occ) ->
-               (tclTHENSI 
-		  (tclTHEN 
-		     (tclTHEN (generalize [(pf_global gls id)]) 
+           | Some (l2,nb_occ) ->
+               (tclTHENSI
+		  (tclTHEN
+		     (tclTHEN (generalize [(pf_global gls id)])
 			(reduce (Pattern [(list_int nb_occ 1 [],l2,
 					   pf_type_of gls l2)]) []))
 		     (general_rewrite_bindings lft2rgt (c,lb))) 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index ba59183cb3..ba519cb2f2 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -10,70 +10,9 @@ open Inductive
 open Evd
 open Environ
 open Proof_trees
-open Stock
 open Clenv
 open Pattern
-
-(* The pattern table for tactics. *)
-
-(* Description: see the interface. *)
-
-(* First part : introduction of term patterns *)
-
-type module_mark = Stock.module_mark
-
-let parse_astconstr s =
-  try 
-    Pcoq.parse_string Pcoq.Constr.constr_eoi s 
-  with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
-    error "Syntax error : not a construction" 
-
-(* Patterns *)
-let parse_pattern s =
-  Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s)
-
-type marked_pattern = (int list * constr_pattern) Stock.stocked
-
-let (pattern_stock : (int list * constr_pattern) Stock.stock) =
-  Stock.make_stock { name = "PATTERN"; proc = parse_pattern }
-
-let put_pat = Stock.stock pattern_stock
-let get_pat tm = snd (Stock.retrieve pattern_stock tm)
-
-let make_module_marker = Stock.make_module_marker
-
-(* Squeletons *)
-let parse_squeleton s =
-  let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_astconstr s) in
-  (collect_metas c, c)
-
-type marked_term = (int list * constr) Stock.stocked
-
-let (squeleton_stock : (int list * constr) Stock.stock) =
-  Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton }
-
-let put_squel = Stock.stock squeleton_stock
-let get_squel_core = Stock.retrieve squeleton_stock
-
-(* Sera mieux avec des noms qualifiés *)
-let get_reference mods s =
-  if list_subset mods (Library.loaded_modules()) then
-    try Declare.global_reference CCI (id_of_string s)
-    with Not_found ->
-      error ("get_reference: "^s^"is not defined in the given modules")
-  else error "The required modules are not open"
-
-let soinstance squel arglist =
-  let mvs,c = get_squel_core squel in
-  let mvb = List.combine mvs arglist in 
-  Reduction.local_strong (Reduction.whd_meta mvb) c
-
-let get_squel m =
-  let mvs, c = get_squel_core m in
-  if mvs = [] then c
-  else errorlabstrm "get_squel"
-    [< Printer.prterm c;
-       'sPC; 'sTR "is not a closed squeleton, use 'soinstance'" >]
+open Coqlib
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -85,8 +24,6 @@ let get_squel m =
   
   -- Eduardo (6/8/97). *)
 
-let mmk = make_module_marker ["Prelude"]
-
 type 'a matching_function = constr -> 'a option
 
 type testing_function  = constr -> bool
@@ -177,9 +114,6 @@ let is_unit_type t = op2bool (match_with_unit_type t)
    inductive binary relation R, so that R has only one constructor
    stablishing its reflexivity.  *)
 
-let refl_rel_pat1 = put_pat mmk "(A : ?)(x:A)(? A x x)"
-let refl_rel_pat2 = put_pat mmk "(x : ?)(? x x)"
-
 let match_with_equation  t =
   let (hdapp,args) = decomp_app t in
   match (kind_of_term hdapp) with
@@ -187,8 +121,8 @@ let match_with_equation  t =
         let constr_types = Global.mind_nf_lc ind in 
         let nconstr = Global.mind_nconstr ind in
 	if nconstr = 1 &&
-           (is_matching (get_pat refl_rel_pat1) constr_types.(0) ||
-            is_matching (get_pat refl_rel_pat2) constr_types.(0)) 
+           (is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0) ||
+            is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0)) 
         then 
 	  Some (hdapp,args)
         else 
@@ -197,11 +131,9 @@ let match_with_equation  t =
 
 let is_equation t = op2bool (match_with_equation  t)
 
-let arrow_pat = put_pat mmk "(?1 -> ?2)"
-
 let match_with_nottype t =
   try
-    match matches (get_pat arrow_pat) t with
+    match matches (build_coq_arrow_pattern ()) t with
       |	[(1,arg);(2,mind)] ->
 	  if is_empty_type mind then Some (mind,arg) else None
       | _ -> anomaly "Incorrect pattern matching" 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 16be20610a..306a740439 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -11,72 +11,8 @@ open Pattern
 open Proof_trees
 (*i*)
 
-(* The pattern table for tactics. *)
-
-(* The idea is that we want to write tactic files which are only
-   "activated" when certain modules are loaded and imported.  Already,
-   the question of how to store the tactics is hard, and we will not
-   address that here.  However, the question arises of how to store
-   the patterns that we will want to use for term-destructuring, and
-   the solution proposed is that we will store patterns with a
-   "module-marker", telling us which modules have to be open in order
-   to use the pattern.  So we will write:
-   \begin{verbatim}
-   let mark = make_module_marker ["<module-name>";<module-name>;...];;
-   let p1 = put_pat mark "<parseable pattern goes here>";;
-   \end{verbatim}
-   And now, we can use [(get p1)]
-   to get the term which corresponds to this pattern, already parsed
-   and with the global names adjusted.
-
-   In other words, we will have the term which we would have had if we
-   had done an:
-   \begin{verbatim}
-        constr_of_com mt_ctxt (initial_sign()) "<text here>"
-   \end{verbatim}
-   except that it will be computed at module-opening time, rather than
-   at tactic-application time.  The ONLY difference will be that
-   no implicit syntax resolution will happen. *)
-
-(* A pattern is intented to be pattern-matched (using functions
-   [somatch] and co), while a squeleton is a term with holes intented to
-   be substituted by [soinstance] *)
-
-(*s First part : introduction of term patterns and term squeletons *)
-
-(* [make_module_marker modl] makes a key from the list of
-   vernacular modules [modl] where names in a pattern or squeleton has
-   to be searched *)
-
-type module_mark = Stock.module_mark
-val make_module_marker : string list -> module_mark
-
-(* [put_pat mmk s] declares a pattern [s] to be parsed using the
-   definitions in the modules associated to the key [mmk] *)
-
-type marked_pattern
-val put_pat            : module_mark -> string -> marked_pattern
-val get_pat            : marked_pattern -> constr_pattern
-
-(* [put_squel mmk s] declares an open term [s] to be parsed using the
-   definitions in the modules associated to the key [mmk] *)
-
-type marked_term
-val put_squel          : module_mark -> string -> marked_term
-
-(*i val get_squel          : marked_term -> constr i*)
-
-(*i Remplacé par Astterm.interp_constrpattern
-val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
-i*)
-
-(* [get_reference mods id] interprets [id] as a global identifier
-   assuming defined in the modules listed in [mods] *)
-
-val get_reference : string list -> string -> constr
-
-(*s Second part : Given a term with second-order variables in it,
-   represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
+(*s Given a term with second-order variables in it,
+   represented by Meta's, and possibly applied using SoApp
    terms, this function will perform second-order, binding-preserving,
    matching, in the case where the pattern is a pattern in the sense
    of Dale Miller.
@@ -92,38 +28,7 @@ val get_reference : string list -> string -> constr
 
    When we reach a second-order application, we ask that the
    intersection of the free-rels of the term and the current stack be
-   contained in the arguments of the application, and in that case, we
-   construct a [DLAM] with the names on the stack. *)
-
-
-(* [dest_somatch c pat] matches [c] against [pat] and returns the resulting
-   assignment of metavariables; it raises [PatternMatchingFailure] if
-   not matchable *)
-(*i
-val dest_somatch : constr -> marked_pattern -> constr list
-
-(* [somatches c pat] just tells if [c] matches against [pat] *)
-
-val somatches    : constr -> marked_pattern -> bool
-
-(* [dest_somatch_conv env sigma] matches up to conversion in
-   environment [(env,sgima)] when constants in pattern are concerned;
-   it raises [PatternMatchingFailure] if not matchable *)
-
-val dest_somatch_conv :
-  Environ.env -> 'a evar_map -> constr -> marked_pattern -> (int * constr) list
-
-(* [somatches_conv env sigma c pat] tells if [c] matches against [pat]
-   up to conversion for constants in patterns *)
-
-val somatches_conv :
-  Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool
-i*)
-
-val soinstance   : marked_term -> constr list -> constr 
-
-(* This works only for squeleton without metavariables *)
-val get_squel    : marked_term -> constr 
+   contained in the arguments of the application *)
 
 val is_imp_term : constr -> bool
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index da43bd0eb2..9b81e87e6a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -52,13 +52,13 @@ open Pattern
 
 let dest_match_eq gls eqn =
   try 
-    pf_matches gls (eq_pattern ()) eqn
+    pf_matches gls (Coqlib.build_coq_eq_pattern ()) eqn
   with PatternMatchingFailure -> 
     (try 
-       pf_matches gls (eqT_pattern ()) eqn
+       pf_matches gls (Coqlib.build_coq_eqT_pattern ()) eqn
      with PatternMatchingFailure -> 
        (try 
-	  pf_matches gls (idT_pattern ()) eqn
+	  pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn
         with PatternMatchingFailure ->
 	  errorlabstrm "dest_match_eq" 
 	    [< 'sTR "no primitive equality here" >]))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f532166d05..08e35f50e2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -21,6 +21,7 @@ open Logic
 open Clenv
 open Tacticals
 open Hipattern
+open Coqlib
 
 exception Bound
 
@@ -58,6 +59,7 @@ let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
   match kind_of_term t with
     | IsProd (_,_,c2)  -> head_constr_bound c2 l 
+    | IsLetIn (_,_,_,c2) -> head_constr_bound c2 l 
     | IsApp (f,args)  -> 
 	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
     | IsConst _        -> t::l
@@ -1558,19 +1560,12 @@ let contradiction_on_hyp id gl =
   else 
     error "Not a contradiction"
 
-let constant dir s = 
-  Declare.global_absolute_reference
-    (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI)
-
-let coq_False = lazy (constant ["Logic"] "False")
-let coq_not = lazy (constant ["Logic"] "not")
-
 (* Absurd *)
 let absurd c gls =
   (tclTHENS
-     (tclTHEN (elim_type (Lazy.force coq_False)) (cut c)) 
+     (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
      ([(tclTHENS
-          (cut (applist(Lazy.force coq_not,[c]))) 
+          (cut (applist(build_coq_not (),[c]))) 
 	  ([(tclTHEN intros
 	       ((fun gl ->
 		   let ida = pf_nth_hyp_id gl 1
@@ -1585,7 +1580,7 @@ let dyn_absurd = function
   | l             -> bad_tactic_args "absurd" l
 
 let contradiction gls = 
-  tclTHENLIST [ intros; elim_type (Lazy.force coq_False); assumption ] gls
+  tclTHENLIST [ intros; elim_type (build_coq_False ()); assumption ] gls
 
 let dyn_contradiction = function
   | []  -> contradiction