diff options
author | 2010-08-27 09:32:12 +0000 | |
---|---|---|
committer | 2010-08-27 09:32:12 +0000 | |
commit | f8bb38326c4fcf8b70da1670d832efd12d667928 (patch) | |
tree | ad85ac51abaa79f3b6195184d754d2a44d86879b | |
parent | d12a7327183054ee5c45f5327105738dcd31c548 (diff) |
* library/Library: Document.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13381 85f007b7-540e-0410-9357-904b9bb8a0f7
-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 44aa05b54..22fecdf63 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; |