aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli1
-rw-r--r--library/globnames.ml8
-rw-r--r--library/globnames.mli2
-rw-r--r--library/goptions.ml32
-rw-r--r--library/goptions.mli5
6 files changed, 18 insertions, 32 deletions
diff --git a/library/global.ml b/library/global.ml
index fbbe09301b..8706238f5a 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -192,8 +192,6 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r
let is_template_polymorphic r = is_template_polymorphic (env ()) r
-let is_template_checked r = is_template_checked (env ()) r
-
let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r
let is_type_in_type r = is_type_in_type (env ()) r
diff --git a/library/global.mli b/library/global.mli
index b6bd69c17c..0198ac5952 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -150,7 +150,6 @@ val is_joined_environment : unit -> bool
val is_polymorphic : GlobRef.t -> bool
val is_template_polymorphic : GlobRef.t -> bool
-val is_template_checked : GlobRef.t -> bool
val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list
val is_type_in_type : GlobRef.t -> bool
diff --git a/library/globnames.ml b/library/globnames.ml
index 63cb2c69bd..e55a7b5499 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -73,13 +73,7 @@ let global_of_constr c = match kind c with
| Var id -> VarRef id
| _ -> raise Not_found
-let is_global c t =
- match c, kind t with
- | ConstRef c, Const (c', _) -> Constant.equal c c'
- | IndRef i, Ind (i', _) -> eq_ind i i'
- | ConstructRef i, Construct (i', _) -> eq_constructor i i'
- | VarRef id, Var id' -> Id.equal id id'
- | _ -> false
+let is_global = Constr.isRefX
let printable_constr_of_global = function
| VarRef id -> mkVar id
diff --git a/library/globnames.mli b/library/globnames.mli
index d61cdd2b64..fb59cbea4e 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -32,6 +32,7 @@ val destIndRef : GlobRef.t -> inductive
val destConstructRef : GlobRef.t -> constructor
val is_global : GlobRef.t -> constr -> bool
+[@@ocaml.deprecated "Use [Constr.isRefX] instead."]
val subst_constructor : substitution -> constructor -> constructor
val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
@@ -44,6 +45,7 @@ val printable_constr_of_global : GlobRef.t -> constr
(** Turn a construction denoting a global reference into a global reference;
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> GlobRef.t
+[@@ocaml.deprecated "Use [Constr.destRef] instead (throws DestKO instead of Not_found)."]
(** {6 Extended global references } *)
diff --git a/library/goptions.ml b/library/goptions.ml
index 6e53bed349..616f6edf72 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -27,7 +27,6 @@ type option_value =
(** Summary of an option status *)
type option_state = {
opt_depr : bool;
- opt_name : string;
opt_value : option_value;
}
@@ -190,7 +189,6 @@ module MakeRefTable =
type 'a option_sig = {
optdepr : bool;
- optname : string;
optkey : option_name;
optread : unit -> 'a;
optwrite : 'a -> unit }
@@ -229,7 +227,7 @@ let warn_deprecated_option =
strbrk " is deprecated")
let declare_option cast uncast append ?(preprocess = fun x -> x)
- { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
+ { optdepr=depr; optkey=key; optread=read; optwrite=write } =
check_key key;
let default = read() in
let change =
@@ -275,7 +273,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
let cread () = cast (read ()) in
let cwrite l v = warn (); change l OptSet (uncast v) in
let cappend l v = warn (); change l OptAppend (uncast v) in
- value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab
+ value_tab := OptionMap.add key (depr, (cread,cwrite,cappend)) !value_tab
let declare_int_option =
declare_option
@@ -298,13 +296,12 @@ let declare_stringopt_option =
(function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
(fun _ _ -> anomaly (Pp.str "async_option."))
-let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) =
+let declare_bool_option_and_ref ~depr ~key ~(value:bool) =
let r_opt = ref value in
let optwrite v = r_opt := v in
let optread () = !r_opt in
let _ = declare_bool_option {
optdepr = depr;
- optname = name;
optkey = key;
optread; optwrite
} in
@@ -323,7 +320,7 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (read,write,append)) ->
+ | Some (depr, (read,write,append)) ->
write locality (check_and_cast v (read ()))
let show_value_type = function
@@ -373,7 +370,7 @@ let set_string_option_append_value_gen ?(locality = OptDefault) key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
- | Some (name, depr, (read,write,append)) ->
+ | Some (depr, (read,write,append)) ->
append locality (check_string_value v (read ()))
let set_int_option_value opt v = set_int_option_value_gen opt v
@@ -382,7 +379,7 @@ let set_string_option_value opt v = set_string_option_value_gen opt v
(* Printing options/tables *)
-let msg_option_value (name,v) =
+let msg_option_value v =
match v with
| BoolValue true -> str "on"
| BoolValue false -> str "off"
@@ -394,19 +391,18 @@ let msg_option_value (name,v) =
(* | IdentValue r -> pr_global_env Id.Set.empty r *)
let print_option_value key =
- let (name, depr, (read,_,_)) = get_option key in
+ let (depr, (read,_,_)) = get_option key in
let s = read () in
match s with
| BoolValue b ->
- Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+ Feedback.msg_notice (prlist_with_sep spc str key ++ str " is " ++ str (if b then "on" else "off"))
| _ ->
- Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+ Feedback.msg_notice (str "Current value of " ++ prlist_with_sep spc str key ++ str " is " ++ msg_option_value s)
let get_tables () =
let tables = !value_tab in
- let fold key (name, depr, (read,_,_)) accu =
+ let fold key (depr, (read,_,_)) accu =
let state = {
- opt_name = name;
opt_depr = depr;
opt_value = read ();
} in
@@ -415,15 +411,15 @@ let get_tables () =
OptionMap.fold fold tables OptionMap.empty
let print_tables () =
- let print_option key name value depr =
- let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
+ let print_option key value depr =
+ let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value value in
if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
else msg ++ fnl ()
in
str "Options:" ++ fnl () ++
OptionMap.fold
- (fun key (name, depr, (read,_,_)) p ->
- p ++ print_option key name (read ()) depr)
+ (fun key (depr, (read,_,_)) p ->
+ p ++ print_option key (read ()) depr)
!value_tab (mt ()) ++
str "Tables:" ++ fnl () ++
List.fold_right
diff --git a/library/goptions.mli b/library/goptions.mli
index 29af196654..e3791dffb1 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -111,8 +111,6 @@ end
type 'a option_sig = {
optdepr : bool;
(** whether the option is DEPRECATED *)
- optname : string;
- (** a short string describing the option *)
optkey : option_name;
(** the low-level name of this option *)
optread : unit -> 'a;
@@ -133,7 +131,7 @@ val declare_stringopt_option: ?preprocess:(string option -> string option) ->
(** Helper to declare a reference controlled by an option. Read-only
as to avoid races. *)
-val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool)
+val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool)
(** {6 Special functions supposed to be used only in vernacentries.ml } *)
@@ -181,7 +179,6 @@ val set_option_value : ?locality:option_locality ->
(** Summary of an option status *)
type option_state = {
opt_depr : bool;
- opt_name : string;
opt_value : option_value;
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 13:13:01 +0000