vi2vo: universes handling finally fixed

Universes that are computed in the vi2vo step are not part of the
outermost module stocked in the vo file.  They are part of the
Library.seg_univ segment and are hence added to the safe env when
the vo file is loaded.

The seg_univ has been augmented.  It is now:
- an array of universe constraints, one for each constant whose opaque
  body was computed in the vi2vo phase.  This is useful only to print
  the constants (and its associated constraints).
- a union of all the constraints that come from proofs generated in the
  vi2vo phase.  This is morally the missing bits in the toplevel module
  body stocked in the vo file, and is there to ease the loading of
  a .vo file (obtained from a .vi file).
- a boolean, false if the file is incomplete (.vi) and true if it is
  complete (.vo obtained via vi2vo).

1 files changed, 8 insertions, 3 deletions

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e2d1e37e9..d70d7d8be 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -8,6 +8,12 @@
 
 open Names
 
+type vodigest =
+  | Dvo_or_vi of Digest.t        (* The digest of the seg_lib part *)
+  | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+val digest_match : actual:vodigest -> required:vodigest -> bool
+
 (** {6 Safe environments } *)
 
 (** Since we are now able to type terms, we can define an abstract type
@@ -120,11 +126,10 @@ val export :
   safe_environment -> DirPath.t ->
     module_path * compiled_library * native_library
 
-val import : compiled_library -> Digest.t ->
+(* Constraints are non empty iff the file is a vi2vo *)
+val import : compiled_library -> Univ.constraints -> vodigest ->
   (module_path * Nativecode.symbol array) safe_transformer
 
-val join_compiled_library : compiled_library -> unit
-
 (** {6 Safe typing judgments } *)
 
 type judgment