aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/namegen.ml6
-rw-r--r--engine/univNames.ml7
-rw-r--r--interp/impargs.ml6
-rw-r--r--interp/notation.ml18
-rw-r--r--interp/reserve.ml2
-rw-r--r--kernel/names.ml75
-rw-r--r--kernel/names.mli22
-rw-r--r--library/coqlib.ml2
-rw-r--r--library/globnames.ml69
-rw-r--r--library/globnames.mli31
-rw-r--r--library/keys.ml6
-rw-r--r--plugins/extraction/extract_env.ml6
-rw-r--r--plugins/extraction/table.ml16
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/setoid_ring/newring.ml4
-rw-r--r--pretyping/arguments_renaming.ml6
-rw-r--r--pretyping/classops.ml10
-rw-r--r--pretyping/recordops.ml14
-rw-r--r--pretyping/reductionops.ml7
-rw-r--r--pretyping/typeclasses.ml40
-rw-r--r--tactics/btermdn.ml2
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/term_dnet.ml2
-rw-r--r--vernac/assumptions.ml34
-rw-r--r--vernac/assumptions.mli5
26 files changed, 216 insertions, 180 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 978f33b683..2a59b914db 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -258,15 +258,15 @@ let restart_subscript id =
forget_subscript id
let visible_ids sigma (nenv, c) =
- let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in
+ let accu = ref (GlobRef.Set_env.empty, Int.Set.empty, Id.Set.empty) in
let rec visible_ids n c = match EConstr.kind sigma c with
| Const _ | Ind _ | Construct _ | Var _ as c ->
let (gseen, vseen, ids) = !accu in
let g = global_of_constr c in
- if not (Refset_env.mem g gseen) then
+ if not (GlobRef.Set_env.mem g gseen) then
begin
try
- let gseen = Refset_env.add g gseen in
+ let gseen = GlobRef.Set_env.add g gseen in
let short = shortest_qualid_of_global Id.Set.empty g in
let dir, id = repr_qualid short in
let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
diff --git a/engine/univNames.ml b/engine/univNames.ml
index a688401741..e861913de2 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -10,7 +10,6 @@
open Names
open Univ
-open Globnames
open Nametab
@@ -51,15 +50,15 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
let empty_binders = Id.Map.empty
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
let universe_binders_of_global ref : universe_binders =
try
- let l = Refmap.find ref !universe_binders_table in l
+ let l = GlobRef.Map.find ref !universe_binders_table in l
with Not_found -> Names.Id.Map.empty
let cache_ubinder (_,(ref,l)) =
- universe_binders_table := Refmap.add ref l !universe_binders_table
+ universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
let subst_ubinder (subst,(ref,l as orig)) =
let ref' = fst (Globnames.subst_global subst ref) in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index e542b818f6..3603367cf1 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -508,11 +508,11 @@ type implicit_discharge_request =
| ImplInteractive of GlobRef.t * implicits_flags *
implicit_interactive_request
-let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
+let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits"
let implicits_of_global ref =
try
- let l = Refmap.find ref !implicits_table in
+ let l = GlobRef.Map.find ref !implicits_table in
try
let rename_l = Arguments_renaming.arguments_names ref in
let rec rename implicits names = match implicits, names with
@@ -527,7 +527,7 @@ let implicits_of_global ref =
with Not_found -> [DefaultImpArgs,[]]
let cache_implicits_decl (ref,imps) =
- implicits_table := Refmap.add ref imps !implicits_table
+ implicits_table := GlobRef.Map.add ref imps !implicits_table
let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l
diff --git a/interp/notation.ml b/interp/notation.ml
index 6b26f66100..a6a14efc87 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -264,7 +264,7 @@ type key =
| Oth
let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
| RefKey _, Oth -> -1
| Oth, RefKey _ -> 1
| Oth, Oth -> 0
@@ -395,7 +395,7 @@ let prim_token_interp_infos =
(* Table from global_reference to backtrack-able informations about
prim_token uninterpretation (in particular uninterpreter unique id). *)
let prim_token_uninterp_infos =
- ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t)
+ ref (GlobRef.Map.empty : (scope_name * prim_token_uid * bool) GlobRef.Map.t)
let hashtbl_check_and_set allow_overwrite uid f h eq =
match Hashtbl.find h uid with
@@ -441,7 +441,7 @@ let cache_prim_token_interpretation (_,infos) =
prim_token_interp_infos :=
String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
List.iter (fun r -> prim_token_uninterp_infos :=
- Refmap.add r (sc,uid,infos.pt_in_match)
+ GlobRef.Map.add r (sc,uid,infos.pt_in_match)
!prim_token_uninterp_infos)
infos.pt_refs
@@ -783,7 +783,7 @@ let uninterp_prim_token c =
| None -> raise Notation_ops.No_match
| Some r ->
try
- let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in
+ let (sc,uid,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
let uninterp = Hashtbl.find prim_token_uninterpreters uid in
match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
| None -> raise Notation_ops.No_match
@@ -924,7 +924,7 @@ let rec update_scopes cls scl = match cls, scl with
| _, [] -> List.map find_scope_class_opt cls
| cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl
-let arguments_scope = ref Refmap.empty
+let arguments_scope = ref GlobRef.Map.empty
type arguments_scope_discharge_request =
| ArgsScopeAuto
@@ -934,7 +934,7 @@ type arguments_scope_discharge_request =
let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
List.iter (Option.iter check_scope) scl;
let initial_stamp = ScopeClassMap.empty in
- arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
+ arguments_scope := GlobRef.Map.add r (scl,cls,initial_stamp) !arguments_scope
let cache_arguments_scope o =
load_arguments_scope 1 o
@@ -1015,13 +1015,13 @@ let declare_arguments_scope local r scl =
let find_arguments_scope r =
try
- let (scl,cls,stamp) = Refmap.find r !arguments_scope in
+ let (scl,cls,stamp) = GlobRef.Map.find r !arguments_scope in
let cur_stamp = !scope_class_map in
if stamp == cur_stamp then scl
else
(* Recent changes in the Bind Scope base, we re-compute the scopes *)
let scl' = update_scopes cls scl in
- arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope;
+ arguments_scope := GlobRef.Map.add r (scl',cls,cur_stamp) !arguments_scope;
scl'
with Not_found -> []
@@ -1350,7 +1350,7 @@ let init () =
notations_key_table := KeyMap.empty;
scope_class_map := initial_scope_class_map;
prim_token_interp_infos := String.Map.empty;
- prim_token_uninterp_infos := Refmap.empty
+ prim_token_uninterp_infos := GlobRef.Map.empty
let _ =
Summary.declare_summary "symbols"
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 071248f01f..edbdf1dbba 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -28,7 +28,7 @@ type key =
(** TODO: share code from Notation *)
let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
| RefKey _, Oth -> -1
| Oth, RefKey _ -> 1
| Oth, Oth -> 0
diff --git a/kernel/names.ml b/kernel/names.ml
index e1d70e8111..933cefe993 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -935,7 +935,7 @@ end
type projection = Projection.t
-module GlobRef = struct
+module GlobRefInternal = struct
type t =
| VarRef of variable (** A reference to the section-context. *)
@@ -951,11 +951,84 @@ module GlobRef = struct
| VarRef v1, VarRef v2 -> Id.equal v1 v2
| (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false
+ 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)
+
+end
+
+module GlobRef = struct
+
+ type t = GlobRefInternal.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. *)
+
+ let equal = GlobRefInternal.equal
+
+ (* By default, [global_reference] are ordered on their canonical part *)
+
+ module Ordered = struct
+ open Constant.CanOrd
+ type t = GlobRefInternal.t
+ let compare gr1 gr2 =
+ GlobRefInternal.global_ord_gen compare ind_ord constructor_ord gr1 gr2
+ let equal gr1 gr2 = GlobRefInternal.global_eq_gen equal eq_ind eq_constructor gr1 gr2
+ let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr
+ end
+
+ module Ordered_env = struct
+ open Constant.UserOrd
+ type t = GlobRefInternal.t
+ let compare gr1 gr2 =
+ GlobRefInternal.global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
+ let equal gr1 gr2 =
+ GlobRefInternal.global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
+ let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr
+ end
+
+ module Map = HMap.Make(Ordered)
+ module Set = Map.Set
+
+ (* Alternative sets and maps indexed by the user part of the kernel names *)
+
+ module Map_env = HMap.Make(Ordered_env)
+ module Set_env = Map_env.Set
+
end
type global_reference = GlobRef.t
[@@ocaml.deprecated "Alias for [GlobRef.t]"]
+
type evaluable_global_reference =
| EvalVarRef of Id.t
| EvalConstRef of Constant.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 1cdf5c2402..2ea8108734 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -645,6 +645,28 @@ module GlobRef : sig
val equal : t -> t -> bool
+ module Ordered : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+ module Ordered_env : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+ module Set_env : CSig.SetS with type elt = t
+ module Map_env : Map.ExtS
+ with type key = t and module Set := Set_env
+
+ module Set : CSig.SetS with type elt = t
+ module Map : Map.ExtS
+ with type key = t and module Set := Set
+
end
type global_reference = GlobRef.t
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/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/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/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 4ede11b5c9..5d3115d8d7 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -710,10 +710,10 @@ let structure_for_compute env sg c =
init false false ~compute:true;
let ast, mlt = Extraction.extract_constr env sg c in
let ast = Mlutil.normalize ast in
- let refs = ref Refset.empty in
- let add_ref r = refs := Refset.add r !refs in
+ let refs = ref GlobRef.Set.empty in
+ let add_ref r = refs := GlobRef.Set.add r !refs in
let () = ast_iter_references add_ref add_ref add_ref ast in
- let refs = Refset.elements !refs in
+ let refs = GlobRef.Set.elements !refs in
let struc = optimize_struct (refs,[]) (mono_environment refs []) in
(flatten_structure struc), ast, mlt
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c3f4cfe654..e05e82af6f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -30,8 +30,8 @@ let capitalize = String.capitalize
(** Sets and maps for [global_reference] that use the "user" [kernel_name]
instead of the canonical one *)
-module Refmap' = Refmap_env
-module Refset' = Refset_env
+module Refmap' = GlobRef.Map_env
+module Refset' = GlobRef.Set_env
(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
@@ -213,12 +213,12 @@ let is_recursor = function
(* NB: here, working modulo name equivalence is ok *)
-let projs = ref (Refmap.empty : (inductive*int) Refmap.t)
-let init_projs () = projs := Refmap.empty
-let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs
-let is_projection r = Refmap.mem r !projs
-let projection_arity r = snd (Refmap.find r !projs)
-let projection_info r = Refmap.find r !projs
+let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t)
+let init_projs () = projs := GlobRef.Map.empty
+let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs
+let is_projection r = GlobRef.Map.mem r !projs
+let projection_arity r = snd (GlobRef.Map.find r !projs)
+let projection_info r = GlobRef.Map.find r !projs
(*s Table of used axioms *)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 85f4939560..286021d68e 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -38,7 +38,7 @@ let compare_gr id1 id2 =
if id1==id2 then 0 else
if id1==dummy_id then 1
else if id2==dummy_id then -1
- else Globnames.RefOrdered.compare id1 id2
+ else GlobRef.Ordered.compare id1 id2
module OrderedInstance=
struct
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2a527da9be..5958fe8203 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -62,7 +62,7 @@ module Hitem=
struct
type t = h_item
let compare (id1,co1) (id2,co2)=
- let c = Globnames.RefOrdered.compare id1 id2 in
+ let c = GlobRef.Ordered.compare id1 id2 in
if c = 0 then
let cmp (i1, c1) (i2, c2) =
let c = Int.compare i1 i2 in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a736eec5e7..b05e1e85b7 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -99,7 +99,7 @@ let protect_tac_in map id =
let rec closed_under sigma cset t =
try
let (gr, _) = Termops.global_of_constr sigma t in
- Refset_env.mem gr cset
+ GlobRef.Set_env.mem gr cset
with Not_found ->
match EConstr.kind sigma t with
| Cast(c,_,_) -> closed_under sigma cset c
@@ -111,7 +111,7 @@ let closed_term args _ = match args with
let t = Option.get (Value.to_constr t) in
let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
Proofview.tclEVARMAP >>= fun sigma ->
- let cs = List.fold_right Refset_env.add l Refset_env.empty in
+ let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in
if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
| _ -> assert false
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 9d4badc60a..b8958ca944 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -21,7 +21,7 @@ module NamedDecl = Context.Named.Declaration
(*i*)
let name_table =
- Summary.ref (Refmap.empty : Name.t list Refmap.t)
+ Summary.ref (GlobRef.Map.empty : Name.t list GlobRef.Map.t)
~name:"rename-arguments"
type req =
@@ -29,7 +29,7 @@ type req =
| ReqGlobal of GlobRef.t * Name.t list
let load_rename_args _ (_, (_, (r, names))) =
- name_table := Refmap.add r names !name_table
+ name_table := GlobRef.Map.add r names !name_table
let cache_rename_args o = load_rename_args 1 o
@@ -68,7 +68,7 @@ let rename_arguments local r names =
let req = if local then ReqLocal else ReqGlobal (r, names) in
Lib.add_anonymous_leaf (inRenameArgs (req, (r, names)))
-let arguments_names r = Refmap.find r !name_table
+let arguments_names r = GlobRef.Map.find r !name_table
let rec rename_prod c = function
| [] -> c
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 332ecd2c91..94da51626f 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -38,7 +38,7 @@ type cl_info_typ = {
type coe_typ = GlobRef.t
-module CoeTypMap = Refmap_env
+module CoeTypMap = GlobRef.Map_env
type coe_info_typ = {
coe_value : GlobRef.t;
@@ -118,7 +118,7 @@ let coercion_tab =
ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
let coercions_in_scope =
- ref Refset_env.empty
+ ref GlobRef.Set_env.empty
module ClPairOrd =
struct
@@ -450,7 +450,7 @@ let load_coercion _ o =
let set_coercion_in_scope (_, c) =
let r = c.coercion_type in
- coercions_in_scope := Refset_env.add r !coercions_in_scope
+ coercions_in_scope := GlobRef.Set_env.add r !coercions_in_scope
let open_coercion i o =
if Int.equal i 1 then begin
@@ -545,7 +545,7 @@ let coercion_of_reference r =
module CoercionPrinting =
struct
type t = coe_typ
- let compare = RefOrdered.compare
+ let compare = GlobRef.Ordered.compare
let encode = coercion_of_reference
let subst = subst_coe_typ
let printer x = pr_global_env Id.Set.empty x
@@ -565,4 +565,4 @@ let hide_coercion coe =
else None
let is_coercion_in_scope r =
- Refset_env.mem r !coercions_in_scope
+ GlobRef.Set_env.mem r !coercions_in_scope
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 2f861c117b..bd41e61b34 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -192,11 +192,11 @@ let rec assoc_pat a = function
let object_table =
- Summary.ref (Refmap.empty : ((cs_pattern * constr) * obj_typ) list Refmap.t)
+ Summary.ref (GlobRef.Map.empty : ((cs_pattern * constr) * obj_typ) list GlobRef.Map.t)
~name:"record-canonical-structs"
let canonical_projections () =
- Refmap.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
+ GlobRef.Map.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
!object_table []
let keep_true_projections projs kinds =
@@ -289,11 +289,11 @@ let warn_redundant_canonical_projection =
let add_canonical_structure warn o =
let lo = compute_canonical_projections warn o in
List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
- let l = try Refmap.find proj !object_table with Not_found -> [] in
+ let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
let ocs = try Some (assoc_pat cs_pat l)
with Not_found -> None
in match ocs with
- | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
+ | None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
| Some (c, cs) ->
let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
@@ -372,18 +372,18 @@ let declare_canonical_structure ref =
add_canonical_structure (check_and_decompose_canonical_structure ref)
let lookup_canonical_conversion (proj,pat) =
- assoc_pat pat (Refmap.find proj !object_table)
+ assoc_pat pat (GlobRef.Map.find proj !object_table)
let decompose_projection sigma c args =
match EConstr.kind sigma c with
| Const (c, u) ->
let n = find_projection_nparams (ConstRef c) in
(** Check if there is some canonical projection attached to this structure *)
- let _ = Refmap.find (ConstRef c) !object_table in
+ let _ = GlobRef.Map.find (ConstRef c) !object_table in
let arg = Stack.nth args n in
arg
| Proj (p, c) ->
- let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in
+ let _ = GlobRef.Map.find (ConstRef (Projection.constant p)) !object_table in
c
| _ -> raise Not_found
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f133eb9963..f4c8a6cd66 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -88,6 +88,7 @@ let set_reduction_effect x funkey =
(** Machinery to custom the behavior of the reduction *)
module ReductionBehaviour = struct
open Globnames
+ open Names
open Libobject
type t = {
@@ -97,7 +98,7 @@ module ReductionBehaviour = struct
}
let table =
- Summary.ref (Refmap.empty : t Refmap.t) ~name:"reductionbehaviour"
+ Summary.ref (GlobRef.Map.empty : t GlobRef.Map.t) ~name:"reductionbehaviour"
type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
type req =
@@ -105,7 +106,7 @@ module ReductionBehaviour = struct
| ReqGlobal of GlobRef.t * (int list * int * flag list)
let load _ (_,(_,(r, b))) =
- table := Refmap.add r b !table
+ table := GlobRef.Map.add r b !table
let cache o = load 1 o
@@ -160,7 +161,7 @@ module ReductionBehaviour = struct
let get r =
try
- let b = Refmap.find r !table in
+ let b = GlobRef.Map.find r !table in
let flags =
if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold]
else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index efb3c339ac..55d9838bbb 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -88,7 +88,7 @@ type typeclass = {
cl_unique : bool;
}
-type typeclasses = typeclass Refmap.t
+type typeclasses = typeclass GlobRef.Map.t
type instance = {
is_class: GlobRef.t;
@@ -99,7 +99,7 @@ type instance = {
is_impl: GlobRef.t;
}
-type instances = (instance Refmap.t) Refmap.t
+type instances = (instance GlobRef.Map.t) GlobRef.Map.t
let instance_impl is = is.is_impl
@@ -121,8 +121,8 @@ let new_instance cl info glob impl =
* states management
*)
-let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
-let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
+let classes : typeclasses ref = Summary.ref GlobRef.Map.empty ~name:"classes"
+let instances : instances ref = Summary.ref GlobRef.Map.empty ~name:"instances"
let typeclass_univ_instance (cl, u) =
assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
@@ -131,7 +131,7 @@ let typeclass_univ_instance (cl, u) =
cl_props = subst_ctx cl.cl_props}
let class_info c =
- try Refmap.find c !classes
+ try GlobRef.Map.find c !classes
with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c))
let global_class_of_constr env sigma c =
@@ -154,7 +154,7 @@ let class_of_constr sigma c =
let is_class_constr sigma c =
try let gr, u = Termops.global_of_constr sigma c in
- Refmap.mem gr !classes
+ GlobRef.Map.mem gr !classes
with Not_found -> false
let rec is_class_type evd c =
@@ -172,7 +172,7 @@ let is_class_evar evd evi =
*)
let load_class (_, cl) =
- classes := Refmap.add cl.cl_impl cl !classes
+ classes := GlobRef.Map.add cl.cl_impl cl !classes
let cache_class = load_class
@@ -336,17 +336,17 @@ type instance_action =
let load_instance inst =
let insts =
- try Refmap.find inst.is_class !instances
- with Not_found -> Refmap.empty in
- let insts = Refmap.add inst.is_impl inst insts in
- instances := Refmap.add inst.is_class insts !instances
+ try GlobRef.Map.find inst.is_class !instances
+ with Not_found -> GlobRef.Map.empty in
+ let insts = GlobRef.Map.add inst.is_impl inst insts in
+ instances := GlobRef.Map.add inst.is_class insts !instances
let remove_instance inst =
let insts =
- try Refmap.find inst.is_class !instances
+ try GlobRef.Map.find inst.is_class !instances
with Not_found -> assert false in
- let insts = Refmap.remove inst.is_impl insts in
- instances := Refmap.add inst.is_class insts !instances
+ let insts = GlobRef.Map.remove inst.is_impl insts in
+ instances := GlobRef.Map.add inst.is_class insts !instances
let cache_instance (_, (action, i)) =
match action with
@@ -464,23 +464,23 @@ let instance_constructor (cl,u) args =
(term, applist (mkConstU cst, pars))
| _ -> assert false
-let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes []
+let typeclasses () = GlobRef.Map.fold (fun _ l c -> l :: c) !classes []
-let cmap_elements c = Refmap.fold (fun k v acc -> v :: acc) c []
+let cmap_elements c = GlobRef.Map.fold (fun k v acc -> v :: acc) c []
let instances_of c =
- try cmap_elements (Refmap.find c.cl_impl !instances) with Not_found -> []
+ try cmap_elements (GlobRef.Map.find c.cl_impl !instances) with Not_found -> []
let all_instances () =
- Refmap.fold (fun k v acc ->
- Refmap.fold (fun k v acc -> v :: acc) v acc)
+ GlobRef.Map.fold (fun k v acc ->
+ GlobRef.Map.fold (fun k v acc -> v :: acc) v acc)
!instances []
let instances r =
let cl = class_info r in instances_of cl
let is_class gr =
- Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
+ GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
let is_instance = function
| ConstRef c ->
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index aca7f6c65e..bfee0422e7 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -28,7 +28,7 @@ type term_label =
| SortLabel
let compare_term_label t1 t2 = match t1, t2 with
-| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2
+| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2
| _ -> Pervasives.compare t1 t2 (** OK *)
type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 43a450ea71..dce1a1bef6 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -288,7 +288,7 @@ let lookup_tacs sigma concl st se =
let sl' = List.stable_sort pri_order_int l' in
List.merge pri_order_int se.sentry_nopat sl'
-module Constr_map = Map.Make(RefOrdered)
+module Constr_map = Map.Make(GlobRef.Ordered)
let is_transparent_gr (ids, csts) = function
| VarRef id -> Id.Pred.mem id ids
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 8bdcc63215..03d2a17eee 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -100,7 +100,7 @@ struct
| DRel, _ -> -1 | _, DRel -> 1
| DSort, DSort -> 0
| DSort, _ -> -1 | _, DSort -> 1
- | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
+ | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2
| DRef _, _ -> -1 | _, DRef _ -> 1
| DCtx (tl1, tr1), DCtx (tl2, tr2)
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index e5d2382e46..0bcd3c64eb 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -213,25 +213,25 @@ let rec traverse current ctx accu t = match Constr.kind t with
and traverse_object ?inhabits (curr, data, ax2ty) body obj =
let data, ax2ty =
- let already_in = Refmap_env.mem obj data in
+ let already_in = GlobRef.Map_env.mem obj data in
match body () with
| None ->
let data =
- if not already_in then Refmap_env.add obj Refset_env.empty data else data in
+ if not already_in then GlobRef.Map_env.add obj GlobRef.Set_env.empty data else data in
let ax2ty =
if Option.is_empty inhabits then ax2ty else
let ty = Option.get inhabits in
- try let l = Refmap_env.find obj ax2ty in Refmap_env.add obj (ty::l) ax2ty
- with Not_found -> Refmap_env.add obj [ty] ax2ty in
+ try let l = GlobRef.Map_env.find obj ax2ty in GlobRef.Map_env.add obj (ty::l) ax2ty
+ with Not_found -> GlobRef.Map_env.add obj [ty] ax2ty in
data, ax2ty
| Some body ->
if already_in then data, ax2ty else
let contents,data,ax2ty =
traverse (label_of obj) Context.Rel.empty
- (Refset_env.empty,data,ax2ty) body in
- Refmap_env.add obj contents data, ax2ty
+ (GlobRef.Set_env.empty,data,ax2ty) body in
+ GlobRef.Map_env.add obj contents data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects the references occurring in the declaration of mutual inductive
definitions. All the constructors and names of a mutual inductive
@@ -244,14 +244,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data
where I_0, I_1, ... are in the same mutual definition and c_ij
are all their constructors. *)
- if Refmap_env.mem firstind_ref data then data, ax2ty else
+ if GlobRef.Map_env.mem firstind_ref data then data, ax2ty else
let mib = lookup_mind mind in
(* Collects references of parameters *)
let param_ctx = mib.mind_params_ctxt in
let nparam = List.length param_ctx in
let accu =
traverse_context label Context.Rel.empty
- (Refset_env.empty, data, ax2ty) param_ctx
+ (GlobRef.Set_env.empty, data, ax2ty) param_ctx
in
(* Build the context of all arities *)
let arities_ctx =
@@ -283,14 +283,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Maps all these dependencies to inductives and constructors*)
let data = Array.fold_left_i (fun n data oib ->
let ind = (mind, n) in
- let data = Refmap_env.add (IndRef ind) contents data in
+ let data = GlobRef.Map_env.add (IndRef ind) contents data in
Array.fold_left_i (fun k data _ ->
- Refmap_env.add (ConstructRef (ind, k+1)) contents data
+ GlobRef.Map_env.add (ConstructRef (ind, k+1)) contents data
) data oib.mind_consnames) data mib.mind_packets
in
data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects references in a rel_context. *)
and traverse_context current ctx accu ctxt =
@@ -307,7 +307,7 @@ and traverse_context current ctx accu ctxt =
let traverse current t =
let () = modcache := MPmap.empty in
- traverse current Context.Rel.empty (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t
+ traverse current Context.Rel.empty (GlobRef.Set_env.empty, GlobRef.Map_env.empty, GlobRef.Map_env.empty) t
(** Hopefully bullet-proof function to recover the type of a constant. It just
ignores all the universe stuff. There are many issues that can arise when
@@ -330,12 +330,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let accu =
if cb.const_typing_flags.check_guarded then accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
in
if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
let t = type_of_constant cb in
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Constant kn,l)) t accu
else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
let t = type_of_constant cb in
@@ -350,7 +350,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
if mind.mind_typing_flags.check_guarded then
accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
in
- Refmap_env.fold fold graph ContextObjectMap.empty
+ GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 751e79d89c..aead345d8c 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -10,7 +10,6 @@
open Names
open Constr
-open Globnames
open Printer
(** Collects all the objects on which a term directly relies, bypassing kernel
@@ -22,8 +21,8 @@ open Printer
*)
val traverse :
Label.t -> constr ->
- (Refset_env.t * Refset_env.t Refmap_env.t *
- (Label.t * Constr.rel_context * types) list Refmap_env.t)
+ (GlobRef.Set_env.t * GlobRef.Set_env.t GlobRef.Map_env.t *
+ (Label.t * Constr.rel_context * types) list GlobRef.Map_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:13:31 +0000