diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-06 13:31:38 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-11 11:04:45 +0100 |
commit | b2a6a5390436e6ba27d604d18e3b4c757875afd1 (patch) | |
tree | d48466472962ee1df4776db9463a98535dcfedb4 /checker/environ.mli | |
parent | 0cd0a3ecdc7f942da153c59369ca3572bd18dd10 (diff) |
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).
Diffstat (limited to 'checker/environ.mli')
-rw-r--r-- | checker/environ.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/environ.mli b/checker/environ.mli index a4162d67f..46b390d0a 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -17,7 +17,7 @@ type env = { env_globals : globals; env_rel_context : rel_context; env_stratification : stratification; - env_imports : Digest.t MPmap.t; + env_imports : Cic.vodigest MPmap.t; } val empty_env : env @@ -26,8 +26,8 @@ val engagement : env -> Cic.engagement option val set_engagement : Cic.engagement -> env -> env (* Digests *) -val add_digest : env -> DirPath.t -> Digest.t -> env -val lookup_digest : env -> DirPath.t -> Digest.t +val add_digest : env -> DirPath.t -> Cic.vodigest -> env +val lookup_digest : env -> DirPath.t -> Cic.vodigest (* de Bruijn variables *) val rel_context : env -> rel_context |