aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml21
-rw-r--r--library/globnames.ml18
-rw-r--r--library/globnames.mli9
-rw-r--r--library/keys.ml17
-rw-r--r--library/lib.ml13
-rw-r--r--library/nametab.ml5
6 files changed, 43 insertions, 40 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 7cd2e50274..b1e4ef2b00 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -13,7 +13,6 @@ open Util
open Pp
open Names
open Libnames
-open Globnames
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
@@ -46,7 +45,7 @@ let has_ref s = CString.Map.mem s !table
let check_ind_ref s ind =
match CString.Map.find s !table with
- | IndRef r -> eq_ind r ind
+ | GlobRef.IndRef r -> eq_ind r ind
| _ -> false
| exception Not_found -> false
@@ -157,32 +156,32 @@ let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp"
let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat"
let nat_path = Libnames.make_path (make_dir datatypes_module_name) (Id.of_string "nat")
-let glob_nat = IndRef (nat_kn,0)
+let glob_nat = GlobRef.IndRef (nat_kn,0)
let path_of_O = ((nat_kn,0),1)
let path_of_S = ((nat_kn,0),2)
-let glob_O = ConstructRef path_of_O
-let glob_S = ConstructRef path_of_S
+let glob_O = GlobRef.ConstructRef path_of_O
+let glob_S = GlobRef.ConstructRef path_of_S
(** Booleans *)
let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool"
-let glob_bool = IndRef (bool_kn,0)
+let glob_bool = GlobRef.IndRef (bool_kn,0)
let path_of_true = ((bool_kn,0),1)
let path_of_false = ((bool_kn,0),2)
-let glob_true = ConstructRef path_of_true
-let glob_false = ConstructRef path_of_false
+let glob_true = GlobRef.ConstructRef path_of_true
+let glob_false = GlobRef.ConstructRef path_of_false
(** Equality *)
let eq_kn = MutInd.make2 logic_module @@ Label.make "eq"
-let glob_eq = IndRef (eq_kn,0)
+let glob_eq = GlobRef.IndRef (eq_kn,0)
let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity"
-let glob_identity = IndRef (identity_kn,0)
+let glob_identity = GlobRef.IndRef (identity_kn,0)
let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq"
-let glob_jmeq = IndRef (jmeq_kn,0)
+let glob_jmeq = GlobRef.IndRef (jmeq_kn,0)
(* Sigma data *)
type coq_sigma_data = {
diff --git a/library/globnames.ml b/library/globnames.ml
index 71447c4b81..acb05f9ac0 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -12,12 +12,14 @@ open Names
open Constr
open Mod_subst
-(*s Global reference is a kernel side type for all references together *)
type global_reference = GlobRef.t =
- | VarRef of variable (** A reference to the section-context. *)
- | ConstRef of Constant.t (** A reference to the environment. *)
- | IndRef of inductive (** A reference to an inductive type. *)
- | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
+ | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"]
+ | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"]
+ | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"]
+ | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"]
+[@@ocaml.deprecated "Use Names.GlobRef.t"]
+
+open GlobRef
let isVarRef = function VarRef _ -> true | _ -> false
let isConstRef = function ConstRef _ -> true | _ -> false
@@ -90,7 +92,7 @@ let printable_constr_of_global = function
type syndef_name = KerName.t
type extended_global_reference =
- | TrueGlobal of global_reference
+ | TrueGlobal of GlobRef.t
| SynDef of syndef_name
(* We order [extended_global_reference] via their user part
@@ -122,6 +124,6 @@ module ExtRefOrdered = struct
end
-type global_reference_or_constr =
- | IsGlobal of global_reference
+type global_reference_or_constr =
+ | IsGlobal of GlobRef.t
| IsConstr of constr
diff --git a/library/globnames.mli b/library/globnames.mli
index 547755b088..fc0de96e36 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -12,12 +12,11 @@ open Names
open Constr
open Mod_subst
-(** {6 Global reference is a kernel side type for all references together } *)
type global_reference = GlobRef.t =
- | VarRef of variable (** A reference to the section-context. *)
- | ConstRef of Constant.t (** A reference to the environment. *)
- | IndRef of inductive (** A reference to an inductive type. *)
- | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
+ | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"]
+ | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"]
+ | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"]
+ | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"]
[@@ocaml.deprecated "Use Names.GlobRef.t"]
val isVarRef : GlobRef.t -> bool
diff --git a/library/keys.ml b/library/keys.ml
index 30ecc9dfdb..9964992433 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -94,7 +94,7 @@ let subst_keys (subst,(k,k')) =
(subst_key subst k, subst_key subst k')
let discharge_key = function
- | KGlob (VarRef _ as g) when Lib.is_in_section g -> None
+ | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None
| x -> Some x
let discharge_keys (_,(k,k')) =
@@ -114,16 +114,15 @@ let declare_equiv_keys ref ref' =
Lib.add_anonymous_leaf (inKeys (ref,ref'))
let constr_key kind c =
- let open Globnames in
- try
- let rec aux k =
+ try
+ let rec aux k =
match kind k with
- | Const (c, _) -> KGlob (ConstRef c)
- | Ind (i, u) -> KGlob (IndRef i)
- | Construct (c,u) -> KGlob (ConstructRef c)
- | Var id -> KGlob (VarRef id)
+ | Const (c, _) -> KGlob (GlobRef.ConstRef c)
+ | Ind (i, u) -> KGlob (GlobRef.IndRef i)
+ | Construct (c,u) -> KGlob (GlobRef.ConstructRef c)
+ | Var id -> KGlob (GlobRef.VarRef id)
| App (f, _) -> aux f
- | Proj (p, _) -> KGlob (ConstRef (Projection.constant p))
+ | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p))
| Cast (p, _, _) -> aux p
| Lambda _ -> KLam
| Prod _ -> KProd
diff --git a/library/lib.ml b/library/lib.ml
index 576e23c4f5..d461644d56 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,7 +13,6 @@ open CErrors
open Util
open Names
open Libnames
-open Globnames
open Libobject
open Context.Named.Declaration
@@ -549,7 +548,7 @@ let empty_segment = {
abstr_uctx = Univ.AUContext.empty;
}
-let section_segment_of_reference = function
+let section_segment_of_reference = let open GlobRef in function
| ConstRef c -> section_segment_of_constant c
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
section_segment_of_mutual_inductive kn
@@ -558,7 +557,7 @@ let section_segment_of_reference = function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).abstr_ctx
-let section_instance = function
+let section_instance = let open GlobRef in function
| VarRef id ->
let eq = function
| Variable {id=id'} -> Names.Id.equal id id'
@@ -647,7 +646,7 @@ let init () =
(* Misc *)
-let mp_of_global = function
+let mp_of_global = let open GlobRef in function
| VarRef id -> !lib_state.path_prefix.Nametab.obj_mp
| ConstRef cst -> Names.Constant.modpath cst
| IndRef ind -> Names.ind_modpath ind
@@ -666,12 +665,12 @@ let rec split_modpath = function
(dp, Names.Label.to_id l :: ids)
let library_part = function
- |VarRef id -> library_dp ()
- |ref -> dp_of_mp (mp_of_global ref)
+ | GlobRef.VarRef id -> library_dp ()
+ | ref -> dp_of_mp (mp_of_global ref)
let discharge_proj_repr =
Projection.Repr.map_npars (fun mind npars ->
- if not (is_in_section (IndRef (mind,0))) then mind, npars
+ if not (is_in_section (GlobRef.IndRef (mind,0))) then mind, npars
else let modlist = replacement_context () in
let _, newpars = Mindmap.find mind (snd modlist) in
mind, npars + Array.length newpars)
diff --git a/library/nametab.ml b/library/nametab.ml
index 71ee7a6d5a..aed7d08ac1 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -392,6 +392,7 @@ let push_xref visibility sp xref =
| _ ->
begin
if ExtRefTab.exists sp !the_ccitab then
+ let open GlobRef in
match ExtRefTab.find sp !the_ccitab with
| TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
TrueGlobal( ConstructRef _) as xref ->
@@ -483,6 +484,7 @@ let completion_canditates qualid =
(* Derived functions *)
let locate_constant qid =
+ let open GlobRef in
match locate_extended qid with
| TrueGlobal (ConstRef kn) -> kn
| _ -> raise Not_found
@@ -517,6 +519,7 @@ let exists_universe kn = UnivTab.exists kn !the_univtab
(* Reverse locate functions ***********************************************)
let path_of_global ref =
+ let open GlobRef in
match ref with
| VarRef id -> make_path DirPath.empty id
| _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
@@ -542,6 +545,7 @@ let path_of_universe mp =
(* Shortest qualid functions **********************************************)
let shortest_qualid_of_global ?loc ctx ref =
+ let open GlobRef in
match ref with
| VarRef id -> make_qualid ?loc DirPath.empty id
| _ ->
@@ -570,6 +574,7 @@ let pr_global_env env ref =
if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
let global_inductive qid =
+ let open GlobRef in
match global qid with
| IndRef ind -> ind
| ref ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:44:05 +0000