Program: add some check_required_library (fix #2592) + some dead code removal

 If these additional checks take too much time, maybe using true laziness
 instead of (fun () -> ...) could help.

 Btw, some other init_constant in Program would deserve preliminary
 check_required_library...

 I've also removed some unused delayed constr, at least one of them
 being erroneous

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

2 files changed, 8 insertions, 25 deletions

diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index cd9028fe87..cf90074c93 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -15,15 +15,16 @@ let ($) f x = f x
 let contrib_name = "Program"
 
 let subtac_dir = [contrib_name]
-let fix_sub_module = "Wf"
-let utils_module = "Utils"
-let fixsub_module = subtac_dir @ [fix_sub_module]
-let utils_module = subtac_dir @ [utils_module]
+let fixsub_module = subtac_dir @ ["Wf"]
+let utils_module = subtac_dir @ ["Utils"]
 let tactics_module = subtac_dir @ ["Tactics"]
 let init_constant dir s () = gen_constant contrib_name dir s
 let init_reference dir s () = gen_reference contrib_name dir s
 
-let fixsub = init_constant fixsub_module "Fix_sub"
+let safe_init_constant md name () =
+  check_required_library md;
+  init_constant md name ()
+
 let ex_pi1 = init_constant utils_module "ex_pi1"
 let ex_pi2 = init_constant utils_module "ex_pi2"
 
@@ -51,13 +52,9 @@ let build_sig () =
 
 let sig_ = build_sig
 
-let fix_proto = init_constant tactics_module "fix_proto"
-let fix_proto_ref () = 
-  match Nametab.global (make_ref "Program.Tactics.fix_proto") with
-  | ConstRef c -> c
-  | _ -> assert false
+let fix_proto = safe_init_constant tactics_module "fix_proto"
 
-let hide_obligation = init_constant tactics_module "obligation"
+let hide_obligation = safe_init_constant tactics_module "obligation"
 
 let eq_ind = init_constant ["Init"; "Logic"] "eq"
 let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
@@ -90,12 +87,6 @@ let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"
 let proj1 = init_constant ["Init"; "Logic"] "proj1"
 let proj2 = init_constant ["Init"; "Logic"] "proj2"
 
-let boolind = init_constant ["Init"; "Datatypes"] "bool"
-let sumboolind = init_constant ["Init"; "Specif"] "sumbool"
-let natind = init_constant ["Init"; "Datatypes"] "nat"
-let intind = init_constant ["ZArith"; "binint"] "Z"
-let existSind = init_constant ["Init"; "Specif"] "sigS"
-
 let existS = build_sigma_type
 
 let prod = build_prod
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 2753a2522c..de96cc602e 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -15,11 +15,9 @@ open Sign
 val ($) : ('a -> 'b) -> 'a -> 'b
 val contrib_name : string
 val subtac_dir : string list
-val fix_sub_module : string
 val fixsub_module : string list
 val init_constant : string list -> string -> constr delayed
 val init_reference : string list -> string -> global_reference delayed
-val fixsub : constr delayed
 val well_founded_ref : global_reference delayed
 val acc_ref : global_reference delayed
 val acc_inv_ref : global_reference delayed
@@ -35,7 +33,6 @@ val build_sig : unit -> coq_sigma_data
 val sig_ : coq_sigma_data delayed
 
 val fix_proto : constr delayed
-val fix_proto_ref : unit -> constant
 
 val hide_obligation : constr delayed
 
@@ -54,11 +51,6 @@ val jmeq_ind : constr delayed
 val jmeq_rec : constr delayed
 val jmeq_refl : constr delayed
 
-val boolind : constr delayed
-val sumboolind : constr delayed
-val natind : constr delayed
-val intind : constr delayed
-val existSind : constr delayed
 val existS : coq_sigma_data delayed
 val prod : coq_sigma_data delayed