Remove dead code in library/lib.ml.

2 files changed, 0 insertions, 39 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 8880a8b15..7218950da 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -506,13 +506,6 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
-let full_replacement_context () = List.map pi2 !sectab
-let full_section_segment_of_constant con =
-  List.map (fun (vars,_,(x,_)) -> fun hyps ->
-    named_of_variable_context
-      (try pi1 (Names.Cmap.find con x)
-       with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
-
 (*************)
 (* Sections. *)
 
@@ -613,15 +606,6 @@ let rec dp_of_mp = function
   |Names.MPbound _ -> library_dp ()
   |Names.MPdot (mp,_) -> dp_of_mp mp
 
-let rec split_mp = function
-  |Names.MPfile dp -> dp, Names.DirPath.empty
-  |Names.MPdot (prfx, lbl) ->
-    let mprec, dprec = split_mp prfx in
-    mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl)
-  |Names.MPbound mbid ->
-    let (_,id,dp) = Names.MBId.repr mbid in
-    library_dp (), Names.DirPath.make [id]
-
 let rec split_modpath = function
   |Names.MPfile dp -> dp, []
   |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid]
@@ -633,20 +617,6 @@ let library_part = function
   |VarRef id -> library_dp ()
   |ref -> dp_of_mp (mp_of_global ref)
 
-let remove_section_part ref =
-  let sp = Nametab.path_of_global ref in
-  let dir,_ = repr_path sp in
-  match ref with
-  | VarRef id ->
-      anomaly (Pp.str "remove_section_part not supported on local variables")
-  | _ ->
-      if is_dirpath_prefix_of dir (cwd ()) then
-        (* Not yet (fully) discharged *)
-        pop_dirpath_n (sections_depth ()) (cwd ())
-      else
-	(* Theorem/Lemma outside its outer section of definition *)
-	dir
-
 (************************)
 (* Discharging names *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 7080b5dba..0a70152ef 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -138,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t
 
 (** Extract the library part of a name even if in a section *)
 val dp_of_mp : Names.module_path -> Names.DirPath.t
-val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t
 val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list
 val library_part :  Globnames.global_reference -> Names.DirPath.t
-val remove_section_part : Globnames.global_reference -> Names.DirPath.t
 
 (** {6 Sections } *)
 
@@ -191,10 +189,3 @@ val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
-
-(* discharging a constant in one go *)
-val full_replacement_context : unit -> Opaqueproof.work_list list
-val full_section_segment_of_constant :
-  Names.constant -> (Context.Named.t -> Context.Named.t) list
-
-