From 330b2eb449c30c53c2578deb7fb6fa464bb9f7ba Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Tue, 24 Apr 2018 22:32:17 -0700 Subject: Don't recurse into closed modules/sections in split_lib. Putting `assert false` in the successful recursive case never triggered. Apparently all users use `split_lib_at_opening` to find open at current nesting level? `split_lib` appears to be dead code currently, might also be candidate for removal. Doing so would allow to simplify `split_lib_gen`, since we only expect one matching element. --- library/lib.ml | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 543cb45bc..0e4106317 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -183,22 +183,11 @@ let split_lib_gen test = | before -> after,equal,before in let rec findeq after = function - | hd :: before -> - if test hd - then Some (collect after [hd] before) - else (match hd with - | (sp,ClosedModule seg) - | (sp,ClosedSection seg) -> - (match findeq after seg with - | None -> findeq (hd::after) before - | Some (sub_after,sub_equal,sub_before) -> - Some (sub_after, sub_equal, (List.append sub_before before))) - | _ -> findeq (hd::after) before) - | [] -> None + | hd :: before when test hd -> collect after [hd] before + | hd :: before -> findeq (hd::after) before + | [] -> user_err Pp.(str "no such entry") in - match findeq [] !lib_state.lib_stk with - | None -> user_err Pp.(str "no such entry") - | Some r -> r + findeq [] !lib_state.lib_stk let eq_object_name (fp1, kn1) (fp2, kn2) = eq_full_path fp1 fp2 && Names.KerName.equal kn1 kn2 -- cgit v1.2.3