diff options
| -rw-r--r-- | library/library.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/library/library.ml b/library/library.ml index 44aa05b54a..22fecdf631 100644 --- a/library/library.ml +++ b/library/library.ml @@ -634,6 +634,12 @@ let save_library_to dir f = try System.marshal_out ch md; flush ch; + (* The table of opaque definitions must be loaded only at will + whereas the digest is loaded all the time. As a consequence, + the digest must be serialized before the table (if we want to + keep the current simple layout of .vo files). This also entails + that the digest does not take opaque terms into account + anymore. *) let di = Digest.file f' in System.marshal_out ch di; System.marshal_out ch table; |