diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-03-25 18:29:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
| commit | 62fb849cf9410ddc2d9f355570f4fb859f3044c3 (patch) | |
| tree | 2f350ca302a46e18840638d20e7ff89beaf2b1f0 /kernel/declareops.mli | |
| parent | ca318cd0d21ce157a3042b600ded99df6face25e (diff) | |
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 9f5197668..6c43bffa9 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -30,6 +30,12 @@ val constant_has_body : constant_body -> bool val body_of_constant : constant_body -> Term.constr option val constraints_of_constant : constant_body -> Univ.constraints +val universes_of_constant : constant_body -> Univ.universe_context + +(** Return the universe context, in case the definition is polymorphic, otherwise + the context is empty. *) + +val universes_of_polymorphic_constant : constant_body -> Univ.universe_context val is_opaque : constant_body -> bool |