diff options
| author | Pierre-Marie Pédrot | 2016-08-21 01:00:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-21 01:00:26 +0200 |
| commit | 6278ce16ab1b8b65c7d1770d265471f594c8e793 (patch) | |
| tree | 4e8eac6336e5a1848fdbb1103932c665cf334cca /interp | |
| parent | 69a35378d37b8eb7e1019d24ab5e0fd27f25b6bc (diff) | |
| parent | 513e194656429b6a9142a3a34095cee2c6f8ee96 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/dumpglob.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 931fc1ca40..1e14eeb81e 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir |