diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-04-24 22:32:17 -0700 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-04-24 23:05:41 -0700 |
| commit | 330b2eb449c30c53c2578deb7fb6fa464bb9f7ba (patch) | |
| tree | b9d03b9dc964f33e3e0ce96ab20811be3aed3fc1 /library/lib.ml | |
| parent | 72d6d5e87759b62dcd9974c87bf59496d27e10b0 (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/lib.ml')
| -rw-r--r-- | library/lib.ml | 19 |
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 |