diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-21 18:24:59 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | 0499f51cedb38eba6b8ecd01ce94ddfb1b6ae9c8 (patch) | |
| tree | eb43b12647b93e52784c9118d77c7a64199989a5 /checker/cic.mli | |
| parent | f7338257584ba69e7e815c7ef9ac0d24f0dec36c (diff) | |
checker and votour ported to new vo format (after -vi2vo)
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 93dc84fa5..8e6c5580d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -182,14 +182,14 @@ type inline = int option type constant_def = | Undef of inline | Def of constr_substituted - | OpaqueDef of lazy_constr Future.computation + | OpaqueDef of lazy_constr type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : Univ.constraints Future.computation; + const_constraints : Univ.constraints; const_native_name : native_name ref; const_inline_code : bool } @@ -387,13 +387,20 @@ type library_disk = { md_deps : library_deps; md_imports : compilation_unit_name array } -type opaque_table = constr array +type opaque_table = constr Future.computation array +type univ_table = Univ.constraints Future.computation array option (** A .vo file is currently made of : 1) a magic number (4 bytes, cf output_binary_int) 2) a marshalled [library_disk] structure 3) a [Digest.t] string (16 bytes) - 4) a marshalled [opaque_table] + 4) a marshalled [univ_table] (* Some if vo was obtained from vi *) 5) a [Digest.t] string (16 bytes) + 6) a marshalled [None] discharge_table (* Some in vi files *) + 7) a [Digest.t] string (16 bytes) + 8) a marshalled [None] todo_table (* Some in vi files *) + 9) a [Digest.t] string (16 bytes) + 10) a marshalled [opaque_table] + 11) a [Digest.t] string (16 bytes) *) |