aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/coqlib.ml26
-rw-r--r--interp/coqlib.mli48
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/firstorder/rules.ml3
-rw-r--r--plugins/fourier/fourierR.ml3
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/indfun_common.ml13
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/nsatz/nsatz.ml6
-rw-r--r--plugins/quote/quote.ml3
-rw-r--r--plugins/romega/const_omega.ml2
-rw-r--r--plugins/rtauto/refl_tauto.ml20
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--tactics/equality.ml5
-rw-r--r--tactics/tactics.ml7
-rw-r--r--vernac/command.ml5
-rw-r--r--vernac/obligations.ml2
18 files changed, 92 insertions, 65 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 9539980f0..9105bdd54 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -32,10 +32,6 @@ let find_reference locstr dir s =
anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp)
let coq_reference locstr dir s = find_reference locstr (coq::dir) s
-let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
-
-let gen_reference = coq_reference
-let gen_constant = coq_constant
let has_suffix_in_dirs dirs ref =
let dir = dirpath (path_of_global ref) in
@@ -68,7 +64,6 @@ let gen_reference_in_modules locstr dirs s =
let gen_constant_in_modules locstr dirs s =
Universes.constr_of_global (gen_reference_in_modules locstr dirs s)
-
(* For tactics/commands requiring vernacular libraries *)
let check_required_library d =
@@ -93,16 +88,16 @@ let check_required_library d =
(* Specific Coq objects *)
let init_reference dir s =
- let d = "Init"::dir in
- check_required_library (coq::d); gen_reference "Coqlib" d s
+ let d = coq::"Init"::dir in
+ check_required_library d; find_reference "Coqlib" d s
let init_constant dir s =
- let d = "Init"::dir in
- check_required_library (coq::d); gen_constant "Coqlib" d s
+ let d = coq::"Init"::dir in
+ check_required_library d; Universes.constr_of_global @@ find_reference "Coqlib" d s
let logic_reference dir s =
- let d = "Logic"::dir in
- check_required_library ("Coq"::d); gen_reference "Coqlib" d s
+ let d = coq::"Logic"::dir in
+ check_required_library d; find_reference "Coqlib" d s
let arith_dir = [coq;"Arith"]
let arith_modules = [arith_dir]
@@ -385,8 +380,8 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
(* The following is less readable but does not depend on parsing *)
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
-let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
-let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
+let coq_jmeq_ref = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq")
+let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true")
let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref"))
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
let coq_exist_ref = lazy (init_reference ["Specif"] "exist")
@@ -397,3 +392,8 @@ let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
let coq_or_ref = lazy (init_reference ["Logic"] "or")
let coq_iff_ref = lazy (init_reference ["Logic"] "iff")
+(* Deprecated *)
+let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
+let gen_reference = coq_reference
+let gen_constant = coq_constant
+
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 1facb47e1..49802089d 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -15,6 +15,25 @@ open Util
(** This module collects the global references, constructions and
patterns of the standard library used in ocaml files *)
+(** The idea is to migrate to rebindable name-based approach, thus the
+ only function this FILE will provide will be:
+
+ [find_reference : string -> global_reference]
+
+ such that [find_reference "core.eq.type"] returns the proper [global_reference]
+
+ [bind_reference : string -> global_reference -> unit]
+
+ will bind a reference.
+
+ A feature based approach would be possible too.
+
+ Contrary to the old approach of raising an anomaly, we expect
+ tactics to gracefully fail in the absence of some primitive.
+
+ This is work in progress, see below.
+*)
+
(** {6 ... } *)
(** [find_reference caller_message [dir;subdir;...] s] returns a global
reference to the name dir.subdir.(...).s; the corresponding module
@@ -25,31 +44,19 @@ open Util
type message = string
val find_reference : message -> string list -> string -> global_reference
-
-(** [coq_reference caller_message [dir;subdir;...] s] returns a
- global reference to the name Coq.dir.subdir.(...).s *)
-
val coq_reference : message -> string list -> string -> global_reference
-(** idem but return a term *)
-
-val coq_constant : message -> string list -> string -> constr
-
-(** Synonyms of [coq_constant] and [coq_reference] *)
-
-val gen_constant : message -> string list -> string -> constr
-val gen_reference : message -> string list -> string -> global_reference
+(** For tactics/commands requiring vernacular libraries *)
+val check_required_library : string list -> unit
(** Search in several modules (not prefixed by "Coq") *)
-val gen_constant_in_modules : string->string list list-> string -> constr
+val gen_constant_in_modules : string->string list list-> string -> constr
val gen_reference_in_modules : string->string list list-> string -> global_reference
+
val arith_modules : string list list
val zarith_base_modules : string list list
val init_modules : string list list
-(** For tactics/commands requiring vernacular libraries *)
-val check_required_library : string list -> unit
-
(** {6 Global references } *)
(** Modules *)
@@ -196,3 +203,12 @@ val coq_sig_ref : global_reference lazy_t
val coq_or_ref : global_reference lazy_t
val coq_iff_ref : global_reference lazy_t
+
+(* Deprecated functions *)
+val coq_constant : message -> string list -> string -> constr
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
+val gen_constant : message -> string list -> string -> constr
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
+val gen_reference : message -> string list -> string -> global_reference
+[@@ocaml.deprecated "Please use Coqlib.find_reference"]
+
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index a0b04ce3b..33a9dd4fd 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -8,7 +8,7 @@ let init_constant dir s =
in
find_constant contrib_name dir s
-let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s)
+let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s)
let get_inductive dir s =
let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 201726d1e..b3017f359 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -26,7 +26,7 @@ open Proofview.Notations
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
+let reference dir s = lazy (Coqlib.coq_reference "CC" dir s)
let _f_equal = reference ["Init";"Logic"] "f_equal"
let _eq_rect = reference ["Init";"Logic"] "eq_rect"
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 86a677007..8c6b5b91d 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -231,7 +231,8 @@ let ll_forall_tac prod backtrack id continue seq=
(* special for compatibility with old Intuition *)
-let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+let constant str = Universes.constr_of_global
+ @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
let defined_connectives=lazy
[AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not")));
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 25d8f8c83..d35e4ec6f 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -285,7 +285,8 @@ let fourier_lineq lineq1 =
let get = Lazy.force
let cget = get
let eget c = EConstr.of_constr (Lazy.force c)
-let constant = Coqlib.gen_constant "Fourier"
+let constant path s = Universes.constr_of_global @@
+ Coqlib.coq_reference "Fourier" path s
(* Standard library *)
open Coqlib
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7f2b21e79..fa246ade8 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -248,10 +248,10 @@ let mk_result ctxt value avoid =
**************************************************)
let coq_True_ref =
- lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True")
+ lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True")
let coq_False_ref =
- lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False")
+ lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False")
(*
[make_discr_match_el \[e1,...en\]] builds match e1,...,en with
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ea985ddec..257f02b70 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -469,13 +469,17 @@ exception ToShow of exn
let jmeq () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
- EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq")
+ EConstr.of_constr @@
+ Universes.constr_of_global @@
+ Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
with e when CErrors.noncritical e -> raise (ToShow e)
let jmeq_refl () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
- EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl")
+ EConstr.of_constr @@
+ Universes.constr_of_global @@
+ Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
with e when CErrors.noncritical e -> raise (ToShow e)
let h_intros l =
@@ -486,7 +490,10 @@ let hrec_id = Id.of_string "hrec"
let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded")
let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
-let well_founded_ltof = function () -> EConstr.of_constr (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
+
+let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@
+ Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
+
let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c46309355..eabad955e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -47,8 +47,8 @@ open Context.Rel.Declaration
(* Ugly things which should not be here *)
-let coq_constant m s =
- EConstr.of_constr (Coqlib.coq_constant "RecursiveDefinition" m s)
+let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@
+ Coqlib.coq_reference "RecursiveDefinition" m s
let arith_Nat = ["Arith";"PeanoNat";"Nat"]
let arith_Lt = ["Arith";"Lt"]
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 632b9dac1..8c3471a98 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -134,8 +134,10 @@ let mul = function
| (Const n,q) when eq_num n num_1 -> q
| (p,q) -> Mul(p,q)
-let tpexpr =
- lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
+let gen_constant msg path s = Universes.constr_of_global @@
+ coq_reference msg path s
+
+let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc")
let ttvar = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEX")
let ttadd = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEadd")
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index c649cfb2c..def9ff3a7 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -118,7 +118,8 @@ open Proofview.Notations
the constants are loaded in the environment *)
let constant dir s =
- EConstr.of_constr (Coqlib.gen_constant "Quote" ("quote"::dir) s)
+ EConstr.of_constr @@ Universes.constr_of_global @@
+ Coqlib.coq_reference "Quote" ("quote"::dir) s
let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index a10ce68b4..f38ca85b6 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -133,7 +133,7 @@ let rec mk_nat = function
let mkListConst c =
let r =
- Coqlib.gen_reference "" ["Init";"Datatypes"] c
+ Coqlib.coq_reference "" ["Init";"Datatypes"] c
in
let inst =
if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|]
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index d580fde29..1b07a8ca8 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -22,28 +22,28 @@ let step_count = ref 0
let node_count = ref 0
-let logic_constant =
- Coqlib.gen_constant "refl_tauto" ["Init";"Logic"]
+let logic_constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s
let li_False = lazy (destInd (logic_constant "False"))
-let li_and = lazy (destInd (logic_constant "and"))
-let li_or = lazy (destInd (logic_constant "or"))
+let li_and = lazy (destInd (logic_constant "and"))
+let li_or = lazy (destInd (logic_constant "or"))
-let pos_constant =
- Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
+let pos_constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s
let l_xI = lazy (pos_constant "xI")
let l_xO = lazy (pos_constant "xO")
let l_xH = lazy (pos_constant "xH")
-let store_constant =
- Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"]
+let store_constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s
let l_empty = lazy (store_constant "empty")
let l_push = lazy (store_constant "push")
-let constant=
- Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"]
+let constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s
let l_Reflect = lazy (constant "Reflect")
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e20e78b1a..d84e62a93 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -283,7 +283,7 @@ let znew_ring_path =
let zltac s =
lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
-let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);;
+let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
(* Ring theory *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 70d6fe90c..f9f9b9dd7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1346,9 +1346,8 @@ let inject_if_homogenous_dependent_pair ty =
pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
- let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
- ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
- let inj2 = EConstr.of_constr inj2 in
+ let inj2 = EConstr.of_constr @@ Universes.constr_of_global @@
+ Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
(* cut with the good equality and prove the requested goal *)
tclTHENLIST
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c713a31fa..617d3d701 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3520,12 +3520,11 @@ let error_ind_scheme s =
let glob c = EConstr.of_constr (Universes.constr_of_global c)
-let coq_eq = lazy (glob (Coqlib.build_coq_eq ()))
+let coq_eq = lazy (glob (Coqlib.build_coq_eq ()))
let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ()))
-let coq_heq = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq"))
-let coq_heq_refl = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl"))
-
+let coq_heq = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq"))
+let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl"))
let mkEq t x y =
mkApp (Lazy.force coq_eq, [| t; x; y |])
diff --git a/vernac/command.ml b/vernac/command.ml
index 8a9bbb884..9382da3fb 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -906,8 +906,9 @@ let subtac_dir = [contrib_name]
let fixsub_module = subtac_dir @ ["Wf"]
let tactics_module = subtac_dir @ ["Tactics"]
-let init_reference dir s () = Coqlib.gen_reference "Command" dir s
-let init_constant dir s () = EConstr.of_constr (Coqlib.gen_constant "Command" dir s)
+let init_reference dir s () = Coqlib.coq_reference "Command" dir s
+let init_constant dir s () = EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "Command" dir s)
+
let make_ref l s = init_reference l s
let fix_proto = init_constant tactics_module "fix_proto"
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 64c156030..be58c67a9 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -260,7 +260,7 @@ let eterm_obligations env name evm fs ?status t ty =
let tactics_module = ["Program";"Tactics"]
let safe_init_constant md name () =
Coqlib.check_required_library ("Coq"::md);
- Coqlib.gen_constant "Obligations" md name
+ Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name)
let hide_obligation = safe_init_constant tactics_module "obligation"
let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 14:58:24 +0000