diff options
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 6ebe691b83..7ff4b657d3 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,6 +21,7 @@ type result = { cook_body : constant_def; cook_type : types; cook_universes : constant_universes; + cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; } |