diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 20:22:37 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 20:24:23 +0100 |
| commit | 7ebe6117789ac3c0d31c8a6ed918fce71b6d2e4b (patch) | |
| tree | 2eb3095e1f80082cde506c286c280ca412eebdca /checker/cic.mli | |
| parent | 6b2ec938010c50dae3ec6c87ff8ea7f2a4012b92 (diff) | |
checker: Change in library on disk values, now using context_sets instead of
constraints only.
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 6ed9a4d25..12146715a 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -433,7 +433,7 @@ type library_disk = { type opaque_table = constr Future.computation array type univ_table = - (Univ.constraints Future.computation array * Univ.constraints * bool) option + (Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool) option (** A .vo file is currently made of : |