diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-13 17:13:44 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-13 17:13:44 +0100 |
commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /library/library.ml | |
parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/library.ml b/library/library.ml index e2832ecdc..840fe563a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -97,7 +97,7 @@ type library_t = { library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_imports : compilation_unit_name array; library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.universe_context_set; + library_extra_univs : Univ.ContextSet.t; } type library_summary = { @@ -360,9 +360,9 @@ type 'a table_status = | Fetched of 'a Future.computation array let opaque_tables = - ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t) + ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) let univ_tables = - ref (LibraryMap.empty : (Univ.universe_context_set table_status) LibraryMap.t) + ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables @@ -408,9 +408,9 @@ let () = type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) - Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool + Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Term.constr Future.computation array +type seg_proofs = Constr.constr Future.computation array let mk_library sd md digests univs = { |