diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml index 42850bc05..9c434fdf1 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -126,7 +126,7 @@ let close_section s = in let (after,_,before) = split_lib sp in lib_stk := before; - add_entry sp (ClosedSection (s,modp,List.rev after)); + add_entry sp (ClosedSection (s,modp,after)); add_frozen_state (); pop_path_prefix () |