diff options
Diffstat (limited to 'vernac/mltop.ml')
| -rw-r--r-- | vernac/mltop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 3620e177fe..8d6268753e 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -394,7 +394,7 @@ let unfreeze_ml_modules x = let _ = Summary.declare_ml_modules_summary - { Summary.freeze_function = (fun _ -> get_loaded_modules ()); + { Summary.freeze_function = (fun ~marshallable -> get_loaded_modules ()); Summary.unfreeze_function = unfreeze_ml_modules; Summary.init_function = reset_loaded_modules } |