aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml3
-rw-r--r--engine/evarutil.mli6
-rw-r--r--engine/evd.ml24
-rw-r--r--engine/evd.mli53
-rw-r--r--engine/nameops.ml26
-rw-r--r--engine/nameops.mli44
-rw-r--r--engine/proofview.ml7
-rw-r--r--engine/proofview.mli9
-rw-r--r--engine/termops.ml3
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml3
-rw-r--r--engine/uState.mli2
-rw-r--r--interp/constrexpr_ops.ml5
-rw-r--r--interp/constrexpr_ops.mli8
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/topconstr.ml23
-rw-r--r--interp/topconstr.mli53
-rw-r--r--library/globnames.ml2
-rw-r--r--library/globnames.mli4
-rw-r--r--library/libnames.ml9
-rw-r--r--library/libnames.mli13
-rw-r--r--library/summary.ml44
-rw-r--r--library/summary.mli20
23 files changed, 0 insertions, 364 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index afedfe180..648f96035 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -875,6 +875,3 @@ let eq_constr_univs_test sigma1 sigma2 t u =
(universes sigma2) fold t u sigma2
in
match ans with None -> false | Some _ -> true
-
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 3ab2d3e34..f271c14ea 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -259,12 +259,6 @@ val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Lo
val meta_counter_summary_tag : int Summary.Dyn.tag
-(** Deprecated *)
-type type_constraint = types option
-[@@ocaml.deprecated "use the version in Evardefine"]
-type val_constraint = constr option
-[@@ocaml.deprecated "use the version in Evardefine"]
-
val e_new_evar :
env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
diff --git a/engine/evd.ml b/engine/evd.ml
index 78d5d4c8f..0c9c3a29b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -132,8 +132,6 @@ end
module Store = Store.Make ()
-type evar = Evar.t
-
let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
type evar_body =
@@ -1206,28 +1204,6 @@ module Monad =
type unsolvability_explanation = SeveralInstancesFound of int
-(** Deprecated *)
-type evar_universe_context = UState.t
-let empty_evar_universe_context = UState.empty
-let union_evar_universe_context = UState.union
-let evar_universe_context_set = UState.context_set
-let evar_universe_context_constraints = UState.constraints
-let evar_context_universe_context = UState.context
-let evar_universe_context_of = UState.of_context_set
-let evar_universe_context_subst = UState.subst
-let add_constraints_context = UState.add_constraints
-let constrain_variables = UState.constrain_variables
-let evar_universe_context_of_binders = UState.of_binders
-let make_evar_universe_context e l =
- let g = Environ.universes e in
- match l with
- | None -> UState.make g
- | Some l -> UState.make_with_initial_binders g l
-let normalize_evar_universe_context_variables = UState.normalize_variables
-let abstract_undefined_variables = UState.abstract_undefined_variables
-let normalize_evar_universe_context = UState.minimize
-let nf_constraints = minimize_universes
-
module MiniEConstr = struct
module ESorts =
diff --git a/engine/evd.mli b/engine/evd.mli
index b2670ee51..c40e925d8 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -33,14 +33,6 @@ type etypes = econstr
(** {5 Existential variables and unification states} *)
-type evar = Evar.t
-[@@ocaml.deprecated "use Evar.t"]
-(** Existential variables. *)
-
-(** {6 Evars} *)
-val string_of_existential : Evar.t -> string
-[@@ocaml.deprecated "use Evar.print"]
-
(** {6 Evar filters} *)
module Filter :
@@ -130,10 +122,6 @@ val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
(** {6 Unification state} **)
-type evar_universe_context = UState.t
-[@@ocaml.deprecated "Alias of UState.t"]
-(** The universe context associated to an evar map *)
-
type evar_map
(** Type of unification state. Essentially a bunch of state-passing data needed
to handle incremental term construction. *)
@@ -529,48 +517,11 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * UState.t
-val evar_universe_context_set : UState.t -> Univ.ContextSet.t
-[@@ocaml.deprecated "Alias of UState.context_set"]
-val evar_universe_context_constraints : UState.t -> Univ.Constraint.t
-[@@ocaml.deprecated "Alias of UState.constraints"]
-val evar_context_universe_context : UState.t -> Univ.UContext.t
-[@@ocaml.deprecated "alias of UState.context"]
-
-val evar_universe_context_of : Univ.ContextSet.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_context_set"]
-val empty_evar_universe_context : UState.t
-[@@ocaml.deprecated "Alias of UState.empty"]
-val union_evar_universe_context : UState.t -> UState.t ->
- UState.t
-[@@ocaml.deprecated "Alias of UState.union"]
-val evar_universe_context_subst : UState.t -> UnivSubst.universe_opt_subst
-[@@ocaml.deprecated "Alias of UState.subst"]
-val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.constrain_variables"]
-
-
-val evar_universe_context_of_binders :
- UnivNames.universe_binders -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_binders"]
-
-val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
-[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"]
val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
(** Raises Not_found if not a name for a universe in this map. *)
val universe_of_name : evar_map -> Id.t -> Univ.Level.t
val universe_binders : evar_map -> UnivNames.universe_binders
-val add_constraints_context : UState.t ->
- Univ.Constraint.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.add_constraints"]
-
-
-val normalize_evar_universe_context_variables : UState.t ->
- Univ.universe_subst in_evar_universe_context
-[@@ocaml.deprecated "Alias of UState.normalize_variables"]
-
-val normalize_evar_universe_context : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.minimize"]
val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
@@ -627,8 +578,6 @@ val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
-val abstract_undefined_variables : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"]
val fix_undefined_variables : evar_map -> evar_map
@@ -636,8 +585,6 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map
-val nf_constraints : evar_map -> evar_map
-[@@ocaml.deprecated "Alias of Evd.minimize_universes"]
val update_sigma_env : evar_map -> env -> evar_map
diff --git a/engine/nameops.ml b/engine/nameops.ml
index 53969cafa..735a59fe5 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -11,10 +11,6 @@
open Util
open Names
-(* Identifiers *)
-
-let pr_id id = Id.print id
-
(* Utilities *)
let code_of_0 = Char.code '0'
@@ -191,28 +187,6 @@ struct
end
-open Name
-
-(* Compatibility *)
-let out_name = get_id
-let name_fold = fold_right
-let name_iter = iter
-let name_app = map
-let name_fold_map = fold_left_map
-let name_cons = cons
-let name_max = pick
-let pr_name = print
-
-let pr_lab l = Label.print l
-
(* Metavariables *)
let pr_meta = Pp.int
let string_of_meta = string_of_int
-
-(* Deprecated *)
-open Libnames
-let default_library = default_library
-let coq_string = coq_string
-let coq_root = coq_root
-let default_root_prefix = default_root_prefix
-
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 96842dfb9..8a93fad8c 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -94,47 +94,3 @@ end
(** Metavariables *)
val pr_meta : Constr.metavariable -> Pp.t
val string_of_meta : Constr.metavariable -> string
-
-val out_name : Name.t -> Id.t
-[@@ocaml.deprecated "Same as [Name.get_id]"]
-
-val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
-[@@ocaml.deprecated "Same as [Name.fold_right]"]
-
-val name_iter : (Id.t -> unit) -> Name.t -> unit
-[@@ocaml.deprecated "Same as [Name.iter]"]
-
-val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.map]"]
-
-val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-[@@ocaml.deprecated "Same as [Name.fold_left_map]"]
-
-val name_max : Name.t -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.pick]"]
-
-val name_cons : Name.t -> Id.t list -> Id.t list
-[@@ocaml.deprecated "Same as [Name.cons]"]
-
-val pr_name : Name.t -> Pp.t
-[@@ocaml.deprecated "Same as [Name.print]"]
-
-val pr_id : Id.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Id.print]"]
-
-val pr_lab : Label.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Label.print]"]
-
-(** Deprecated stuff to libnames *)
-val default_library : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_library]"]
-
-val coq_root : module_ident (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_root]"]
-
-val coq_string : string (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_string]"]
-
-val default_root_prefix : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"]
-
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 54237ceb4..fdb0a215d 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1085,8 +1085,6 @@ module Goal = struct
self : Evar.t ; (* for compatibility with old-style definitions *)
}
- let assume (gl : t) = (gl : t)
-
let print { sigma; self } = { Evd.it = self; sigma }
let state { state=state } = state
@@ -1274,11 +1272,6 @@ module V82 = struct
- (* Returns the open goals of the proofview together with the evar_map to
- interpret them. *)
- let goals { comb = comb ; solution = solution; } =
- { Evd.it = List.map drop_state comb ; sigma = solution }
-
let top_goals initial { solution=solution; } =
let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
{ Evd.it = goals ; sigma=solution; }
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 1905686fe..970bf6773 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -495,10 +495,6 @@ module Goal : sig
(** Type of goals. *)
type t
- (** Assume that you do not need the goal to be normalized. *)
- val assume : t -> t
- [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"]
-
(** Normalises the argument goal. *)
val normalize : t -> t tactic
@@ -589,11 +585,6 @@ module V82 : sig
(in chronological order of insertion). *)
val grab : proofview -> proofview
- (* Returns the open goals of the proofview together with the evar_map to
- interpret them. *)
- val goals : proofview -> Evar.t list Evd.sigma
- [@@ocaml.deprecated "Use [Proofview.proofview]"]
-
val top_goals : entry -> proofview -> Evar.t list Evd.sigma
(* returns the existential variable used to start the proof *)
diff --git a/engine/termops.ml b/engine/termops.ml
index c52f96079..51fc59289 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -974,9 +974,6 @@ let count_occurrences sigma m t =
countrec m t;
!n
-(* Synonymous *)
-let occur_term = dependent
-
let pop t = EConstr.Vars.lift (-1) t
(***************************)
diff --git a/engine/termops.mli b/engine/termops.mli
index e2ddcd36e..bb3cbb6a8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -113,8 +113,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int
val collect_metas : Evd.evar_map -> constr -> int list
val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
-val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
-[@@ocaml.deprecated "alias of Termops.dependent"]
(* Substitution of metavariables *)
type meta_value_map = (metavariable * Constr.constr) list
diff --git a/engine/uState.ml b/engine/uState.ml
index 844eb390b..15cf4d4c1 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -663,6 +663,3 @@ let update_sigma_env uctx env =
let pr_weak prl {uctx_weak_constraints=weak} =
let open Pp in
prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
-
-(** Deprecated *)
-let normalize = minimize
diff --git a/engine/uState.mli b/engine/uState.mli
index 11aaaf389..d1678a155 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -137,8 +137,6 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
(** Universe minimization *)
val minimize : t -> t
-val normalize : t -> t
-[@@ocaml.deprecated "Alias of UState.minimize"]
type universe_decl =
(Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 4ee13c961..3eb5acfc5 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -600,8 +600,3 @@ let _ = Goptions.declare_bool_option {
Goptions.optread = (fun () -> !asymmetric_patterns);
Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
}
-
-(************************************************************************)
-(* Deprecated *)
-let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c
-let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d038bd71a..2df9e5a8c 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -60,14 +60,6 @@ val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr
val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
(** Apply a list of pattern arguments to a pattern *)
-(** @deprecated variant of mkCLambdaN *)
-val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-[@@ocaml.deprecated "deprecated variant of mkCLambdaN"]
-
-(** @deprecated variant of mkCProdN *)
-val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-[@@ocaml.deprecated "deprecated variant of mkCProdN"]
-
(** {6 Destructors}*)
val coerce_reference_to_id : reference -> Id.t
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 61313acc4..37a327a7d 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -9,7 +9,6 @@ Smartlocate
Constrexpr_ops
Ppextend
Dumpglob
-Topconstr
Reserve
Impargs
Implicit_quantifiers
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
deleted file mode 100644
index 7d2d75d9c..000000000
--- a/interp/topconstr.ml
+++ /dev/null
@@ -1,23 +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 Constrexpr_ops
-
-let asymmetric_patterns = asymmetric_patterns
-let error_invalid_pattern_notation = error_invalid_pattern_notation
-let split_at_annot = split_at_annot
-let ntn_loc = ntn_loc
-let patntn_loc = patntn_loc
-let map_constr_expr_with_binders = map_constr_expr_with_binders
-let fold_constr_expr_with_binders = fold_constr_expr_with_binders
-let ids_of_cases_indtype = ids_of_cases_indtype
-let occur_var_constr_expr = occur_var_constr_expr
-let free_vars_of_constr_expr = free_vars_of_constr_expr
-let replace_vars_constr_expr = replace_vars_constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
deleted file mode 100644
index c86502015..000000000
--- a/interp/topconstr.mli
+++ /dev/null
@@ -1,53 +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 Names
-open Constrexpr
-
-(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops *)
-val asymmetric_patterns : bool ref
-[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"]
-
-(** Utilities on constr_expr *)
-val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list
-[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"]
-
-val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
-[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"]
-val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
-[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"]
-
-(** For cases pattern parsing errors *)
-val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
-[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"]
-
-(*************************************************************************)
-val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr
-[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
-
-val free_vars_of_constr_expr : constr_expr -> Id.Set.t
-[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
-
-val occur_var_constr_expr : Id.t -> constr_expr -> bool
-[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"]
-
-(** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
-[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"]
-
-(** Used in typeclasses *)
-val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
- ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
-[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"]
-
-val map_constr_expr_with_binders :
- (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
- 'a -> constr_expr -> constr_expr
-[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"]
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/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/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-05-15 04:50:06 +0000