12 files changed, 5 insertions, 151 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 0d32853116..c1a673edf0 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 6b78d12baf..6383a1f8f6 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 2fe35ebccd..15fcd5bdd9 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/heads.ml b/library/heads.ml
index 198672a0a1..3d5f6a6ff0 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -129,7 +129,7 @@ let compute_head = function
    let cb = Environ.lookup_constant cst env in
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
-     if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
+     if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body
      then Global.body_of_constant cst else None
    in
      (match body with
diff --git a/library/keys.ml b/library/keys.ml
index 89363455d7..3cadcb6472 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/lib.ml b/library/lib.ml
index 0e41063174..128b27e757 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -51,7 +51,7 @@ let subst_objects subst seg =
       if obj' == obj then node else
 	(id, obj')
   in
-    List.smartmap subst_one seg
+    List.Smart.map subst_one seg
 
 (*let load_and_subst_objects i prefix subst seg =
   List.rev (List.fold_left (fun seg (id,obj as node) ->
@@ -569,13 +569,11 @@ let close_section () =
   in
   let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  let full_olddir = !lib_state.path_prefix.obj_dir in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
-  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
-  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
 
 (* State and initialization. *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index d847313221..8d5a02a299 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)
 
@@ -174,8 +170,6 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (* this won't last long I hope! *)
 
 let eq_op op1 op2 =
   DirPath.equal op1.obj_dir op2.obj_dir &&
@@ -187,7 +181,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
 | DirModule op1, DirModule op2 -> eq_op op1 op2
-| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2
 | _ -> false
 
 type reference_r =
@@ -243,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 9dad26129e..5f69b1f0f5 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
 
@@ -125,8 +119,6 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
   global_dir_reference -> global_dir_reference -> bool
@@ -157,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 72db3b31cb..cfae074843 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -50,39 +50,10 @@ type 'id move_location =
   | MoveFirst
   | MoveLast (** can be seen as "no move" when doing intro *)
 
-(** Sorts *)
-
-type 'a glob_sort_gen =
-  | GProp (** representation of [Prop] literal *)
-  | GSet  (** representation of [Set] literal *)
-  | GType of 'a (** representation of [Type] literal *)
-
-type 'a universe_kind =
-  | UAnonymous
-  | UUnknown
-  | UNamed of 'a
-
-type level_info = Libnames.reference universe_kind
-type glob_level = level_info glob_sort_gen
-type glob_constraint = glob_level * Univ.constraint_type * glob_level
-
-type sort_info = (Libnames.reference * int) option list
-type glob_sort = sort_info glob_sort_gen
-
 (** A synonym of [Evar.t], also defined in Term *)
 
 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 =
@@ -141,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/nametab.ml b/library/nametab.ml
index 2046bf7580..995f447061 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -432,7 +432,6 @@ let full_name_module qid =
 let locate_section qid =
   match locate_dir qid with
     | DirOpenSection { obj_dir; _ } -> obj_dir
-    | DirClosedSection dir -> dir
     | _ -> raise Not_found
 
 let locate_all qid =
diff --git a/library/summary.ml b/library/summary.ml
index 7ef19fbfb4..9b22945919 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 ed6c26b190..7d91a79188 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