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 /kernel/cooking.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 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 934b7c6b50..c98fb0bc3a 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,14 +21,14 @@ type 'opaque result = { cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; - cook_private_univs : Univ.ContextSet.t option; cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; } val cook_constant : recipe -> Opaqueproof.opaque result -val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr +val cook_constr : Opaqueproof.cooking_info list -> int -> + (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes) val cook_inductive : Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry |