diff options
Diffstat (limited to 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 07c6f37fab..89b5c60ad5 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -20,7 +20,7 @@ type inline = bool type result = { cook_body : constr Mod_subst.substituted constant_def; cook_type : types; - cook_universes : constant_universes; + cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; |