From 575da16f72ac125ba7e50b1bfe63302dee639973 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 May 2016 18:19:15 +0200 Subject: Adding a local type-in-type flag in kernel declarations. --- kernel/indtypes.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/indtypes.ml') 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; } (************************************************************************) -- cgit v1.2.3