From b2a6a5390436e6ba27d604d18e3b4c757875afd1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Mar 2014 13:31:38 +0100 Subject: 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). --- checker/cic.mli | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'checker/cic.mli') diff --git a/checker/cic.mli b/checker/cic.mli index 8e6c5580d..bfea85327 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -362,7 +362,11 @@ type nativecode_symb_array type compilation_unit_name = DirPath.t -type library_info = compilation_unit_name * Digest.t +type vodigest = + | Dvo 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 *) + +type library_info = compilation_unit_name * vodigest type library_deps = library_info array @@ -388,7 +392,8 @@ type library_disk = { md_imports : compilation_unit_name array } type opaque_table = constr Future.computation array -type univ_table = Univ.constraints Future.computation array option +type univ_table = + (Univ.constraints Future.computation array * Univ.constraints * bool) option (** A .vo file is currently made of : -- cgit v1.2.3