factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )

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

7 files changed, 25 insertions, 73 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index ca4a249685..420d0e4db8 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -32,13 +32,13 @@ exception Not_an_eq
 
 let fail()=raise Not_an_eq
     
-let constr_of_string s () =
-  constr_of_reference (Nametab.locate (qualid_of_string s))
 
-let eq2eqT_theo = constr_of_string "Coq.Logic.Eqdep_dec.eq2eqT"
-let eqT2eq_theo = constr_of_string "Coq.Logic.Eqdep_dec.eqT2eq"
-let congr_theo = constr_of_string "Coq.cc.CC.Congr_nodep"
-let congr_dep_theo = constr_of_string "Coq.cc.CC.Congr_dep"
+let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
+
+let eq2eqT_theo = constant ["Logic";"Eqdep_dec"] "eq2eqT"
+let eqT2eq_theo = constant ["Logic";"Eqdep_dec"] "eqT2eq"
+let congr_theo = constant ["cc";"CC"] "Congr_nodep"
+let congr_dep_theo = constant ["cc";"CC"] "Congr_dep"
 
 let fresh_id1=id_of_string "eq1" and fresh_id2=id_of_string "eq2"
     
@@ -104,7 +104,7 @@ let st_wrap theo tac=
 (* generate an adhoc tactic following the proof tree  *)
 
 let rec proof_tac uf axioms=function
-    Ax id->(fun gl->(st_wrap (eq2eqT_theo ()) (exact_check (mkVar id)) gl))
+    Ax id->(fun gl->(st_wrap (Lazy.force eq2eqT_theo) (exact_check (mkVar id)) gl))
   | Refl t->reflexivity
   | Trans (p1,p2)->let t=(make_term (snd (type_proof uf axioms p1))) in
       (tclTHENS (transitivity t) 
@@ -118,14 +118,14 @@ let rec proof_tac uf axioms=function
 	and ts2=(make_term s2) and tt2=(make_term t2) in
       let typ1=pf_type_of gl ts1 and typ2=pf_type_of gl ts2 in
       let (typb,_,_)=(eq_type_of_term gl.it.evar_concl) in
-      let act=mkApp ((congr_theo ()),[|typ2;typb;ts1;tt1;ts2;tt2|]) in
+      let act=mkApp ((Lazy.force congr_theo),[|typ2;typb;ts1;tt1;ts2;tt2|]) in
       tclORELSE 
 	(tclTHENS 
 	   (apply act)	 
 	   [(proof_tac uf axioms p1);(proof_tac uf axioms p2)])		
 	   (tclTHEN
 	      (let p=mkLambda(destProd typ1) in
-	      let acdt=mkApp((congr_dep_theo ()),[|typ2;p;ts1;tt1;ts2|]) in 
+	      let acdt=mkApp((Lazy.force congr_dep_theo),[|typ2;p;ts1;tt1;ts2|]) in 
 	      apply acdt) (proof_tac uf axioms p1))
 	gl)
 
@@ -139,7 +139,7 @@ let cc_tactic gl_sg=
   match (cc_proof prb) with
     None->errorlabstrm  "CC" [< str "CC couldn't solve goal" >] 
   | Some (p,uf,axioms)->let tac=proof_tac uf axioms p in
-    (tclORELSE (st_wrap (eqT2eq_theo ()) tac)
+    (tclORELSE (st_wrap (Lazy.force eqT2eq_theo) tac)
        (fun _->errorlabstrm  "CC" 
 	  [< str "CC doesn't know how to handle dependent equality." >]) gl_sg)
 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index c67dea9aa9..6f5668b191 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -26,15 +26,7 @@ open Tacexpr
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 (* Construction of constants *)
-let constant dir s =
-  let dir = make_dirpath
-    (List.map id_of_string (List.rev ("Coq"::"field"::dir))) in
-  let id = id_of_string s in
-  try 
-    Declare.global_reference_in_absolute_module dir id
-  with Not_found ->
-    anomaly ("Field: cannot find "^
-	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
+let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s
 
 (* To deal with the optional arguments *)
 let constr_of_opt a opt =
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index f99b548ee1..d90b064193 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -66,22 +66,12 @@ let prNamedLConstr s lc =
     prNamedLConstr_aux lc
   end
 
-
-(* tire de const\_omega.ml *)
-let constant dir s =
-  try
-    Declare.global_absolute_reference
-      (Libnames.make_path
-        (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
-        (Names.id_of_string s))
-  with e -> print_endline (String.concat "." dir); print_endline s; 
-            raise e
-(* fin const\_omega.ml *)
+let constant =Coqlib.gen_constant "Funind"
 
 let mkEq typ c1 c2 = 
   mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|])
 let mkRefl typ c1 = 
-  mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"),
+  mkApp ((constant ["Init"; "Logic"] "refl_equal"),
          [| typ; c1|])
 
 let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
@@ -183,7 +173,7 @@ let nth_dep_constructor indtype n =
   build_dependent_constructor cstr_sum,  cstr_sum.cs_nargs
 
 
-let coq_refl_equal = lazy(constant ["Coq"; "Init"; "Logic"] "refl_equal")
+let coq_refl_equal = lazy(constant ["Init"; "Logic"] "refl_equal")
 
 let rec buildrefl_from_eqs eqs = 
   match eqs with 
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index b5d6601c66..9b1602ad41 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -222,29 +222,21 @@ let (imply_elim2: pbp_rule) = function
            make_clears clear_names]))
   | _ -> None;;
 
-let reference dir s =
-  let dir = make_dirpath
-              (List.map id_of_string (List.rev ("Coq"::"Init"::[dir]))) in
-  let id = id_of_string s in
-  try 
-    Nametab.absolute_reference (Libnames.make_path dir id)
-  with Not_found ->
-    anomaly ("Coqlib: cannot find "^
-	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
-
-let constant dir s =  constr_of_reference (reference dir s);;
+let reference dir s = Coqlib.gen_reference "Pbp" ("Init"::dir) s
+
+let constant dir s =  Coqlib.gen_constant "Pbp" ("Init"::dir) s
 
 let andconstr: unit -> constr = Coqlib.build_coq_and;;
-let prodconstr () = constant "Datatypes" "prod";;
+let prodconstr () = constant ["Datatypes"] "prod";;
 let exconstr = Coqlib.build_coq_ex;;
-let exTconstr () = constant "Logic_Type" "exT";;
-let sigconstr () = constant "Specif" "sig";;
+let exTconstr () = constant ["Logic_Type"] "exT";;
+let sigconstr () = constant ["Specif"] "sig";;
 let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ;;
 let orconstr = Coqlib.build_coq_or;;
 let sumboolconstr = Coqlib.build_coq_sumbool;;
-let sumconstr() = constant "Datatypes" "sum";;
+let sumconstr() = constant ["Datatypes"] "sum";;
 let notconstr = Coqlib.build_coq_not;;
-let notTconstr () = constant "Logic_Type" "notT";;
+let notTconstr () = constant ["Logic_Type"] "notT";;
 
 let is_matching_local a b = is_matching (pattern_of_constr a) b;;
 
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 93408cbc46..6f988076ef 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -193,14 +193,7 @@ 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 dir s =
-  let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in
-  let id = id_of_string s in
-  try 
-    Declare.global_reference_in_absolute_module dir id
-  with Not_found ->
-    anomaly ("Coq_omega: cannot find "^
-	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
+let constant = Coqlib.gen_constant "Omega"
 
 let arith_constant dir = constant ("Arith"::dir)
 let zarith_constant dir = constant ("ZArith"::dir)
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index a2798d7a75..393eff193f 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -119,15 +119,7 @@ open Tacexpr
   We do that lazily, because this code can be linked before
   the constants are loaded in the environment *)
 
-let constant dir s =
-  let dir = make_dirpath
-              (List.map id_of_string (List.rev ("Coq"::"ring"::dir))) in
-  let id = id_of_string s in
-  try 
-    Declare.global_reference_in_absolute_module dir id
-  with Not_found ->
-    anomaly ("Quote: cannot find "^
-	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
+let constant dir s = Coqlib.gen_constant "Quote" ("ring"::dir) s
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
 let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index f4848c729e..c360f795a2 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -38,14 +38,7 @@ open Quote
 let mt_evd = Evd.empty
 let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
 
-let constant dir s =
-  let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in
-  let id = id_of_string s in
-  try 
-    Declare.global_reference_in_absolute_module dir id
-  with Not_found ->
-    anomaly ("Ring: cannot find "^
-	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
+let constant = Coqlib.gen_constant "Ring"
 
 (* Ring theory *)
 let coq_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Ring_Theory")