diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:11:41 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:16:49 +0100 |
| commit | 20c98eab851210702b39e1c66e005acfc351d8dd (patch) | |
| tree | 957aab7aadfda8c10f251ff9d83f3f5b05c07dc5 /engine/uState.mli | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
Proper nametab handling of global universe names
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
Diffstat (limited to 'engine/uState.mli')
| -rw-r--r-- | engine/uState.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index 16fba41e0..2c39e85f7 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -154,3 +154,4 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) val pr_uctx_level : t -> Univ.Level.t -> Pp.t +val reference_of_level : t -> Univ.Level.t -> Libnames.reference |