aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 31f983595..10b4915a2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -446,10 +446,6 @@ let section_segment_of_constant con =
let section_segment_of_mutual_inductive kn =
Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
-let rec list_mem_assoc x = function
- | [] -> raise Not_found
- | (a, _) :: l -> Names.Id.equal a x || list_mem_assoc x l
-
let section_instance = function
| VarRef id ->
if List.exists (fun (id',_,_,_) -> Names.id_eq id id')