aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-04-24 22:32:17 -0700
committerGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-04-24 23:05:41 -0700
commit330b2eb449c30c53c2578deb7fb6fa464bb9f7ba (patch)
treeb9d03b9dc964f33e3e0ce96ab20811be3aed3fc1 /library
parent72d6d5e87759b62dcd9974c87bf59496d27e10b0 (diff)
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.
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml19
1 files changed, 4 insertions, 15 deletions
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