From a21e1bb60f579baec910d4c3d8e8434501470b6d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 May 2019 16:42:48 +0200
Subject: Move the Discharge module into the kernel.

---
 library/lib.ml  | 3 ---
 library/lib.mli | 1 -
 2 files changed, 4 deletions(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 4be288ed20..daa41eca65 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -474,9 +474,6 @@ let extract_hyps (secs,ohyps) =
 let instance_from_variable_context =
   List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
 
-let named_of_variable_context =
-  List.map fst
-
 let name_instance inst =
   (* FIXME: this should probably be done at an upper level, by storing the
      name information in the section data structure. *)
diff --git a/library/lib.mli b/library/lib.mli
index 5da76961a6..c19c3bf7fa 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -168,7 +168,6 @@ type abstr_info = private {
 }
 
 val instance_from_variable_context : variable_context -> Id.t array
-val named_of_variable_context : variable_context -> Constr.named_context
 
 val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
-- 
cgit v1.2.3