diff options
| author | Pierre-Marie Pédrot | 2019-06-04 13:44:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-17 15:20:02 +0200 |
| commit | 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a (patch) | |
| tree | 8016562d06949b981a3e58e71103b02aea7f1c44 /library/global.mli | |
| parent | 7e47fea5ce050c8129ba2d6f94e93fbc29763a3b (diff) | |
Allow to delay polymorphic opaque constants.
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/library/global.mli b/library/global.mli index c36cec3511..34b6c52833 100644 --- a/library/global.mli +++ b/library/global.mli @@ -100,13 +100,16 @@ val mind_of_delta_kn : KerName.t -> MutInd.t val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> + (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option (** 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 : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant_body : Opaqueproof.indirect_accessor -> + Opaqueproof.opaque Declarations.constant_body -> + (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** {6 Compiled libraries } *) |