diff options
| author | Gaëtan Gilbert | 2019-06-17 22:57:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-17 22:57:33 +0200 |
| commit | 459fc67f4a40ff82a7694f9afafb3ac303d74554 (patch) | |
| tree | 9c1607700b3689c36de0daf0427f5e95aeb5b55c /kernel/cooking.mli | |
| parent | d886dff0857702fc4524779980ee6b7e9688c1d4 (diff) | |
| parent | 621201858125632496fd11f431529187d69cfdc6 (diff) | |
Merge PR #10362: Kernel-side delaying of polymorphic opaque constants
Reviewed-by: SkySkimmer
Reviewed-by: gares
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 5a75c691a7..671cdf51fe 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 -> + (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes) val cook_inductive : Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry |