aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml11
-rw-r--r--library/globnames.ml2
-rw-r--r--library/globnames.mli4
-rw-r--r--library/keys.ml4
-rw-r--r--library/libnames.ml9
-rw-r--r--library/libnames.mli13
-rw-r--r--library/misctypes.ml16
-rw-r--r--library/summary.ml44
-rw-r--r--library/summary.mli20
9 files changed, 2 insertions, 121 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 0d3285311..c1a673edf 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -74,14 +74,3 @@ type logical_kind =
| IsAssumption of assumption_object_kind
| IsDefinition of definition_object_kind
| IsProof of theorem_kind
-
-(** Recursive power of type declarations *)
-
-type recursivity_kind = Declarations.recursivity_kind =
- | Finite (** = inductive *)
- [@ocaml.deprecated "Please use [Declarations.Finite"]
- | CoFinite (** = coinductive *)
- [@ocaml.deprecated "Please use [Declarations.CoFinite"]
- | BiFinite (** = non-recursive, like in "Record" definitions *)
- [@ocaml.deprecated "Please use [Declarations.BiFinite"]
-[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
diff --git a/library/globnames.ml b/library/globnames.ml
index 6b78d12ba..6383a1f8f 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -87,8 +87,6 @@ let printable_constr_of_global = function
| ConstructRef sp -> mkConstruct sp
| IndRef sp -> mkInd sp
-let reference_of_constr = global_of_constr
-
let global_eq_gen eq_cst eq_ind eq_cons x y =
x == y ||
match x, y with
diff --git a/library/globnames.mli b/library/globnames.mli
index 2fe35ebcc..15fcd5bdd 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -49,10 +49,6 @@ val printable_constr_of_global : GlobRef.t -> constr
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> GlobRef.t
-(** Obsolete synonyms for constr_of_global and global_of_constr *)
-val reference_of_constr : constr -> GlobRef.t
-[@@ocaml.deprecated "Alias of Globnames.global_of_constr"]
-
module RefOrdered : sig
type t = GlobRef.t
val compare : t -> t -> int
diff --git a/library/keys.ml b/library/keys.ml
index 89363455d..3cadcb647 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -11,9 +11,9 @@
(** Keys for unification and indexing *)
open Names
-open Term
-open Globnames
+open Constr
open Libobject
+open Globnames
type key =
| KGlob of GlobRef.t
diff --git a/library/libnames.ml b/library/libnames.ml
index 4ceea480d..8d5a02a29 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -15,8 +15,6 @@ open Names
(**********************************************)
-let pr_dirpath sl = DirPath.print sl
-
(*s Operations on dirpaths *)
let split_dirpath d = match DirPath.repr d with
@@ -80,8 +78,6 @@ let dirpath_of_string s =
in
DirPath.make path
-let string_of_dirpath = Names.DirPath.to_string
-
module Dirset = Set.Make(DirPath)
module Dirmap = Map.Make(DirPath)
@@ -240,8 +236,3 @@ let default_library = Names.DirPath.initial (* = ["Top"] *)
let coq_string = "Coq"
let coq_root = Id.of_string coq_string
let default_root_prefix = DirPath.empty
-
-(* Deprecated synonyms *)
-
-let make_short_qualid = qualid_of_ident
-let qualid_of_sp = qualid_of_path
diff --git a/library/libnames.mli b/library/libnames.mli
index 81e5bc5b1..5f69b1f0f 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -14,12 +14,6 @@ open Names
(** {6 Dirpaths } *)
val dirpath_of_string : string -> DirPath.t
-val pr_dirpath : DirPath.t -> Pp.t
-[@@ocaml.deprecated "Alias for DirPath.print"]
-
-val string_of_dirpath : DirPath.t -> string
-[@@ocaml.deprecated "Alias for DirPath.to_string"]
-
(** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *)
val pop_dirpath : DirPath.t -> DirPath.t
@@ -155,10 +149,3 @@ val coq_string : string (** "Coq" *)
(** This is the default root prefix for developments which doesn't
mention a root *)
val default_root_prefix : DirPath.t
-
-(** Deprecated synonyms *)
-val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *)
-[@@ocaml.deprecated "Alias for qualid_of_ident"]
-
-val qualid_of_sp : full_path -> qualid (** = qualid_of_path *)
-[@@ocaml.deprecated "Alias for qualid_of_sp"]
diff --git a/library/misctypes.ml b/library/misctypes.ml
index b5d30559d..cfae07484 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -54,16 +54,6 @@ type 'id move_location =
type existential_key = Evar.t
-(** Case style, shared with Term *)
-
-type case_style = Constr.case_style =
- | LetStyle
- | IfStyle
- | LetPatternStyle
- | MatchStyle
- | RegularStyle (** infer printing form from number of constructor *)
-[@@ocaml.deprecated "Alias for Constr.case_style"]
-
(** Casts *)
type 'a cast_type =
@@ -122,9 +112,3 @@ type multi =
| UpTo of int
| RepeatStar
| RepeatPlus
-
-type ('a, 'b) gen_universe_decl = {
- univdecl_instance : 'a; (* Declared universes *)
- univdecl_extensible_instance : bool; (* Can new universes be added *)
- univdecl_constraints : 'b; (* Declared constraints *)
- univdecl_extensible_constraints : bool (* Can new constraints be added *) }
diff --git a/library/summary.ml b/library/summary.ml
index 7ef19fbfb..9b2294591 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -75,20 +75,6 @@ let freeze_summaries ~marshallable : frozen =
ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
}
-let unfreeze_single name state =
- let decl =
- try String.Map.find name !sum_map
- with
- | Not_found ->
- CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name)
- in
- try decl.unfreeze_function state
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- Feedback.msg_warning
- Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
- iraise e
-
let warn_summary_out_of_scope =
let name = "summary-out-of-scope" in
let category = "dev" in
@@ -142,36 +128,6 @@ let remove_from_summary st tag =
let summaries = String.Map.remove id st.summaries in
{st with summaries}
-(** Selective freeze *)
-
-type frozen_bits = Dyn.t String.Map.t
-
-let freeze_summary ~marshallable ?(complement=false) ids =
- let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in
- String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map
-
-let unfreeze_summary = String.Map.iter unfreeze_single
-
-let surgery_summary { summaries; ml_module } bits =
- let summaries =
- String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in
- { summaries; ml_module }
-
-let project_summary { summaries; ml_module } ?(complement=false) ids =
- String.Map.filter (fun name _ -> complement <> List.(mem name ids)) summaries
-
-let pointer_equal l1 l2 =
- let ptr_equal d1 d2 =
- let Dyn.Dyn (t1, x1) = d1 in
- let Dyn.Dyn (t2, x2) = d2 in
- match Dyn.eq t1 t2 with
- | None -> false
- | Some Refl -> x1 == x2
- in
- let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in
- CList.for_all2eq
- (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
-
(** All-in-one reference declaration + registration *)
let ref_tag ?(freeze=fun _ r -> r) ~name x =
diff --git a/library/summary.mli b/library/summary.mli
index ed6c26b19..7d91a7918 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -91,25 +91,5 @@ val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen
val project_from_summary : frozen -> 'a Dyn.tag -> 'a
val remove_from_summary : frozen -> 'a Dyn.tag -> frozen
-(** The type [frozen_bits] is a snapshot of some of the registered
- tables. It is DEPRECATED in favor of the typed projection
- version. *)
-
-type frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-
-[@@@ocaml.warning "-3"]
-val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val unfreeze_summary : frozen_bits -> unit
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val surgery_summary : frozen -> frozen_bits -> frozen
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val pointer_equal : frozen_bits -> frozen_bits -> bool
-[@@ocaml.deprecated "Please use the typed version of summary projection"]
-[@@@ocaml.warning "+3"]
-
(** {6 Debug} *)
val dump : unit -> (int * string) list
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 22:40:41 +0000