aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml2
-rw-r--r--library/dischargedhypsmap.ml21
-rw-r--r--library/dischargedhypsmap.mli19
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli2
-rw-r--r--library/globnames.ml69
-rw-r--r--library/globnames.mli31
-rw-r--r--library/goptions.ml2
-rw-r--r--library/keys.ml6
-rw-r--r--library/library.mllib1
-rw-r--r--library/nametab.ml48
11 files changed, 37 insertions, 168 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 408e259196..36a9598f36 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -47,7 +47,7 @@ let gen_reference_in_modules locstr dirs s =
let dirs = List.map make_dir dirs in
let qualid = qualid_of_string s in
let all = Nametab.locate_all qualid in
- let all = List.sort_uniquize RefOrdered_env.compare all in
+ let all = List.sort_uniquize GlobRef.Ordered_env.compare all in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
| [x] -> x
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
deleted file mode 100644
index abcdb93a27..0000000000
--- a/library/dischargedhypsmap.ml
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Libnames
-
-type discharged_hyps = full_path list
-
-let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis"
-
-let set_discharged_hyps sp hyps =
- discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
-
-let get_discharged_hyps sp =
- try Spmap.find sp !discharged_hyps_map with Not_found -> []
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
deleted file mode 100644
index c70677225b..0000000000
--- a/library/dischargedhypsmap.mli
+++ /dev/null
@@ -1,19 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Libnames
-
-type discharged_hyps = full_path list
-
-(** Discharged hypothesis. Here we store the discharged hypothesis of each
- constant or inductive type declaration. *)
-
-val set_discharged_hyps : full_path -> discharged_hyps -> unit
-val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/global.ml b/library/global.ml
index e833f71142..5872126a12 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -271,8 +271,8 @@ let with_global f =
push_context_set false ctx; a
(* spiwack: register/unregister functions for retroknowledge *)
-let register field value by_clause =
- globalize0 (Safe_typing.register field value by_clause)
+let register field value =
+ globalize0 (Safe_typing.register field value)
let register_inline c = globalize0 (Safe_typing.register_inline c)
diff --git a/library/global.mli b/library/global.mli
index 2819c187ed..6aeae9fd02 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t
(** {6 Retroknowledge } *)
val register :
- Retroknowledge.field -> Constr.constr -> Constr.constr -> unit
+ Retroknowledge.field -> GlobRef.t -> unit
val register_inline : Constant.t -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index 6383a1f8f6..6bbdd36489 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -87,65 +87,14 @@ let printable_constr_of_global = function
| ConstructRef sp -> mkConstruct sp
| IndRef sp -> mkInd sp
-let global_eq_gen eq_cst eq_ind eq_cons x y =
- x == y ||
- match x, y with
- | ConstRef cx, ConstRef cy -> eq_cst cx cy
- | IndRef indx, IndRef indy -> eq_ind indx indy
- | ConstructRef consx, ConstructRef consy -> eq_cons consx consy
- | VarRef v1, VarRef v2 -> Id.equal v1 v2
- | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false
-
-let global_ord_gen ord_cst ord_ind ord_cons x y =
- if x == y then 0
- else match x, y with
- | VarRef v1, VarRef v2 -> Id.compare v1 v2
- | VarRef _, _ -> -1
- | _, VarRef _ -> 1
- | ConstRef cx, ConstRef cy -> ord_cst cx cy
- | ConstRef _, _ -> -1
- | _, ConstRef _ -> 1
- | IndRef indx, IndRef indy -> ord_ind indx indy
- | IndRef _, _ -> -1
- | _ , IndRef _ -> 1
- | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
-
-let global_hash_gen hash_cst hash_ind hash_cons gr =
- let open Hashset.Combine in
- match gr with
- | ConstRef c -> combinesmall 1 (hash_cst c)
- | IndRef i -> combinesmall 2 (hash_ind i)
- | ConstructRef c -> combinesmall 3 (hash_cons c)
- | VarRef id -> combinesmall 4 (Id.hash id)
-
-(* By default, [global_reference] are ordered on their canonical part *)
-
-module RefOrdered = struct
- open Constant.CanOrd
- type t = global_reference
- let compare gr1 gr2 =
- global_ord_gen compare ind_ord constructor_ord gr1 gr2
- let equal gr1 gr2 = global_eq_gen equal eq_ind eq_constructor gr1 gr2
- let hash gr = global_hash_gen hash ind_hash constructor_hash gr
-end
-
-module RefOrdered_env = struct
- open Constant.UserOrd
- type t = global_reference
- let compare gr1 gr2 =
- global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
- let equal gr1 gr2 =
- global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
- let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr
-end
-
-module Refmap = HMap.Make(RefOrdered)
-module Refset = Refmap.Set
+module RefOrdered = Names.GlobRef.Ordered
+module RefOrdered_env = Names.GlobRef.Ordered_env
-(* Alternative sets and maps indexed by the user part of the kernel names *)
+module Refmap = Names.GlobRef.Map
+module Refset = Names.GlobRef.Set
-module Refmap_env = HMap.Make(RefOrdered_env)
-module Refset_env = Refmap_env.Set
+module Refmap_env = Names.GlobRef.Map_env
+module Refset_env = Names.GlobRef.Set_env
(* Extended global references *)
@@ -164,14 +113,14 @@ module ExtRefOrdered = struct
let equal x y =
x == y ||
match x, y with
- | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.equal rx ry
+ | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry
| SynDef knx, SynDef kny -> KerName.equal knx kny
| (TrueGlobal _ | SynDef _), _ -> false
let compare x y =
if x == y then 0
else match x, y with
- | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry
+ | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry
| SynDef knx, SynDef kny -> KerName.compare knx kny
| TrueGlobal _, SynDef _ -> -1
| SynDef _, TrueGlobal _ -> 1
@@ -179,7 +128,7 @@ module ExtRefOrdered = struct
open Hashset.Combine
let hash = function
- | TrueGlobal gr -> combinesmall 1 (RefOrdered_env.hash gr)
+ | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr)
| SynDef kn -> combinesmall 2 (KerName.hash kn)
end
diff --git a/library/globnames.mli b/library/globnames.mli
index 15fcd5bdd9..45ee069b06 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
open Names
open Constr
open Mod_subst
@@ -49,27 +48,21 @@ val printable_constr_of_global : GlobRef.t -> constr
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> GlobRef.t
-module RefOrdered : sig
- type t = GlobRef.t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val hash : t -> int
-end
+module RefOrdered = Names.GlobRef.Ordered
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered"]
-module RefOrdered_env : sig
- type t = GlobRef.t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val hash : t -> int
-end
+module RefOrdered_env = Names.GlobRef.Ordered_env
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"]
-module Refset : CSig.SetS with type elt = GlobRef.t
-module Refmap : Map.ExtS
- with type key = GlobRef.t and module Set := Refset
+module Refset = Names.GlobRef.Set
+[@@ocaml.deprecated "Use Names.GlobRef.Set"]
+module Refmap = Names.GlobRef.Map
+[@@ocaml.deprecated "Use Names.GlobRef.Map"]
-module Refset_env : CSig.SetS with type elt = GlobRef.t
-module Refmap_env : Map.ExtS
- with type key = GlobRef.t and module Set := Refset_env
+module Refset_env = GlobRef.Set_env
+[@@ocaml.deprecated "Use Names.GlobRef.Set_env"]
+module Refmap_env = GlobRef.Map_env
+[@@ocaml.deprecated "Use Names.GlobRef.Map_env"]
(** {6 Extended global references } *)
diff --git a/library/goptions.ml b/library/goptions.ml
index eafcb8fea6..dcbc46ab72 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -412,7 +412,7 @@ let print_tables () =
if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
else msg ++ fnl ()
in
- str "Synchronous options:" ++ fnl () ++
+ str "Options:" ++ fnl () ++
OptionMap.fold
(fun key (name, depr, (read,_,_)) p ->
p ++ print_option key name (read ()) depr)
diff --git a/library/keys.ml b/library/keys.ml
index 3cadcb6472..a74d13c600 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -31,7 +31,7 @@ module KeyOrdered = struct
let hash gr =
match gr with
- | KGlob gr -> 8 + RefOrdered.hash gr
+ | KGlob gr -> 8 + GlobRef.Ordered.hash gr
| KLam -> 0
| KLet -> 1
| KProd -> 2
@@ -43,14 +43,14 @@ module KeyOrdered = struct
let compare gr1 gr2 =
match gr1, gr2 with
- | KGlob gr1, KGlob gr2 -> RefOrdered.compare gr1 gr2
+ | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
| _, KGlob _ -> -1
| KGlob _, _ -> 1
| k, k' -> Int.compare (hash k) (hash k')
let equal k1 k2 =
match k1, k2 with
- | KGlob gr1, KGlob gr2 -> RefOrdered.equal gr1 gr2
+ | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
| _, KGlob _ -> false
| KGlob _, _ -> false
| k, k' -> k == k'
diff --git a/library/library.mllib b/library/library.mllib
index 9cacaba4a7..8f694f4a31 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -11,7 +11,6 @@ Loadpath
Library
States
Kindops
-Dischargedhypsmap
Goptions
Decls
Keys
diff --git a/library/nametab.ml b/library/nametab.ml
index a3b3ca6e74..840cf8e380 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -279,10 +279,10 @@ module ExtRefTab = Make(FullPath)(ExtRefEqual)
module MPTab = Make(FullPath)(MPEqual)
type ccitab = ExtRefTab.t
-let the_ccitab = ref (ExtRefTab.empty : ccitab)
+let the_ccitab = Summary.ref ~name:"ccitab" (ExtRefTab.empty : ccitab)
type mptab = MPTab.t
-let the_modtypetab = ref (MPTab.empty : mptab)
+let the_modtypetab = Summary.ref ~name:"modtypetab" (MPTab.empty : mptab)
module DirPath' =
struct
@@ -303,7 +303,7 @@ module DirTab = Make(DirPath')(GlobDir)
(* If we have a (closed) module M having a submodule N, than N does not
have the entry in [the_dirtab]. *)
type dirtab = DirTab.t
-let the_dirtab = ref (DirTab.empty : dirtab)
+let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
type universe_id = DirPath.t * int
@@ -314,7 +314,7 @@ struct
end
module UnivTab = Make(FullPath)(UnivIdEqual)
type univtab = UnivTab.t
-let the_univtab = ref (UnivTab.empty : univtab)
+let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
(* Reversed name tables ***************************************************)
@@ -322,14 +322,14 @@ let the_univtab = ref (UnivTab.empty : univtab)
module Globrevtab = HMap.Make(ExtRefOrdered)
type globrevtab = full_path Globrevtab.t
-let the_globrevtab = ref (Globrevtab.empty : globrevtab)
+let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)
type mprevtab = DirPath.t MPmap.t
-let the_modrevtab = ref (MPmap.empty : mprevtab)
+let the_modrevtab = Summary.ref ~name:"modrevtab" (MPmap.empty : mprevtab)
type mptrevtab = full_path MPmap.t
-let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
+let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevtab)
module UnivIdOrdered =
struct
@@ -344,7 +344,7 @@ end
module UnivIdMap = HMap.Make(UnivIdOrdered)
type univrevtab = full_path UnivIdMap.t
-let the_univrevtab = ref (UnivIdMap.empty : univrevtab)
+let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab)
(* Push functions *********************************************************)
@@ -546,38 +546,6 @@ let global_inductive qid =
(********************************************************************)
-(********************************************************************)
-(* Registration of tables as a global table and rollback *)
-
-type frozen = ccitab * dirtab * mptab * univtab
- * globrevtab * mprevtab * mptrevtab * univrevtab
-
-let freeze _ : frozen =
- !the_ccitab,
- !the_dirtab,
- !the_modtypetab,
- !the_univtab,
- !the_globrevtab,
- !the_modrevtab,
- !the_modtyperevtab,
- !the_univrevtab
-
-let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) =
- the_ccitab := ccit;
- the_dirtab := dirt;
- the_modtypetab := mtyt;
- the_univtab := univt;
- the_globrevtab := globr;
- the_modrevtab := modr;
- the_modtyperevtab := mtyr;
- the_univrevtab := univr
-
-let _ =
- Summary.declare_summary "names"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = Summary.nop }
-
(* Deprecated synonyms *)
let extended_locate = locate_extended
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:22:55 +0000