diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 19:58:09 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 19:58:09 -0500 |
| commit | 42cd40e4edcc29804d1b73d8cb076f8578ce66fa (patch) | |
| tree | 37ef6e88abc417ac2a3b7697edac8423b4dc8033 /checker/safe_typing.mli | |
| parent | 7c102bb3a3798a234701fdc28a8e8ec28ee2549c (diff) | |
Checker was forgetting to register global universes introduced by opaque
proofs.
Diffstat (limited to 'checker/safe_typing.mli')
| -rw-r--r-- | checker/safe_typing.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index e16e64e6a..892a8d2cc 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -15,6 +15,6 @@ val get_env : unit -> env val set_engagement : engagement -> unit val import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit val unsafe_import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit |