diff options
| author | Pierre-Marie Pédrot | 2019-05-21 19:00:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | 2fa3dc389a58ca4a390b99995d82e6c089add163 (patch) | |
| tree | 32ec7005bbbee5acfef94679fd4d475fc647e068 /kernel/environ.mli | |
| parent | b245a6c46bc3ef70142e8a165f6cde54265b941e (diff) | |
Move body_of_constant_body to Global and specialize its uses.
This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.
The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index f6cd41861e..2abcea148a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses -> polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t -(** Returns the body of the constant if it has any, and the polymorphic context - it lives in. For monomorphic constant, the latter is empty, and for - polymorphic constants, the term contains De Bruijn universe variables that - need to be instantiated. *) -val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option - (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) |