diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-11 14:06:40 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-11 14:06:40 +0200 |
| commit | 9368a1572f55dea66aa21edf140b84d883c5fccc (patch) | |
| tree | 0d754f7b59584ed50459d94b12acb7d6a4f43c6e /library | |
| parent | 9091187bad0e609211060032880e4688e2cafbef (diff) | |
| parent | 330b2eb449c30c53c2578deb7fb6fa464bb9f7ba (diff) | |
Merge PR #7341: Don't recurse into closed modules/sections in split_lib.
Diffstat (limited to 'library')
| -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 |