aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-20 09:09:23 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-20 11:39:41 +0200
commit97abe11a5ea271dcde5bd0aedd69056be22220eb (patch)
tree532c401fa08f5f2b493a51816974e1757282ec67
parent1fda29d0179d60c83ead5db6e3062511aba7d264 (diff)
Remove dead code in library/lib.ml.
-rw-r--r--library/lib.ml30
-rw-r--r--library/lib.mli9
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
-
-