diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 19:11:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | 012f5fb722a9d5dcef82c800aa54ed50c0a58957 (patch) | |
| tree | fbe0e3ae6901faba4f14b8cd4dbda019ce9a7829 /library/global.mli | |
| parent | b8a7222e670f69e024d50394afd88204e15d1b29 (diff) | |
Safe API for accessing universe constraints of global references.
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index 754fa1516..5ddf54b4a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -141,7 +141,7 @@ val type_of_global_unsafe : Globnames.global_reference -> Constr.types [Evarutil.new_global] and [Retyping.get_type_of]. *) (** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.universe_context +val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context (** {6 Retroknowledge } *) |