diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b74788d21..34771034c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -923,6 +923,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_universes = ctx; mind_private = prv; mind_checked_positive = is_checked; + mind_unsafe_universes = type_in_type env; } (************************************************************************) |