diff options
| -rw-r--r-- | kernel/declarations.mli | 4 | ||||
| -rw-r--r-- | kernel/declareops.ml | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 6 | ||||
| -rw-r--r-- | kernel/environ.mli | 2 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 1 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 1 | ||||
| -rw-r--r-- | library/global.ml | 8 | ||||
| -rw-r--r-- | library/global.mli | 1 |
8 files changed, 25 insertions, 0 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 8b42a90e4..639cd061b 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -73,6 +73,7 @@ type constant_universes = Univ.universe_context type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) + check_universes : bool; (** If [false] universe constraints are not checked *) } (* some contraints are in constant_constraints, some other may be in @@ -192,6 +193,9 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) + + mind_unsafe_universes : bool; (** generated with the type-in-type flag *) + } (** {6 Module declarations } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 28f7e69cd..5caf052ac 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -16,6 +16,7 @@ open Context.Rel.Declaration let safe_flags = { check_guarded = true; + check_universes = true; } (** {6 Arities } *) @@ -261,6 +262,7 @@ let subst_mind_body sub mib = mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_checked_positive = mib.mind_checked_positive; + mind_unsafe_universes = mib.mind_unsafe_universes; } let inductive_instance mib = diff --git a/kernel/environ.ml b/kernel/environ.ml index d8493d9ba..032e71359 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -328,6 +328,9 @@ let polymorphic_pconstant (cst,u) env = if Univ.Instance.is_empty u then false else polymorphic_constant cst env +let type_in_type_constant cst env = + not (lookup_constant cst env).const_typing_flags.check_universes + let template_polymorphic_constant cst env = match (lookup_constant cst env).const_type with | TemplateArity _ -> true @@ -357,6 +360,9 @@ let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false else polymorphic_ind ind env +let type_in_type_ind (mind,i) env = + (lookup_mind mind env).mind_unsafe_universes + let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true diff --git a/kernel/environ.mli b/kernel/environ.mli index 520389954..7ce1cea27 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -136,6 +136,7 @@ val evaluable_constant : constant -> env -> bool (** New-style polymorphism *) val polymorphic_constant : constant -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool +val type_in_type_constant : constant -> env -> bool (** Old-style polymorphism *) val template_polymorphic_constant : constant -> env -> bool @@ -183,6 +184,7 @@ val lookup_mind : mutual_inductive -> env -> mutual_inductive_body (** New-style polymorphism *) val polymorphic_ind : inductive -> env -> bool val polymorphic_pind : pinductive -> env -> bool +val type_in_type_ind : inductive -> env -> bool (** Old-style polymorphism *) val template_polymorphic_ind : inductive -> env -> bool 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; } (************************************************************************) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f0c116d27..a7c6ef057 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -269,6 +269,7 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) = + let flags = { flags with check_universes = flags.check_universes && not (type_in_type env) } in let open Context.Named.Declaration in let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in diff --git a/library/global.ml b/library/global.ml index f4ee62b6e..e456841f8 100644 --- a/library/global.ml +++ b/library/global.ml @@ -244,6 +244,14 @@ let is_template_polymorphic r = | IndRef ind -> Environ.template_polymorphic_ind ind env | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env +let is_type_in_type r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> Environ.type_in_type_constant c env + | IndRef ind -> Environ.type_in_type_ind ind env + | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env + let current_dirpath () = Safe_typing.current_dirpath (safe_env ()) diff --git a/library/global.mli b/library/global.mli index 7c6cecb4e..91fc55918 100644 --- a/library/global.mli +++ b/library/global.mli @@ -116,6 +116,7 @@ val is_joined_environment : unit -> bool val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool +val is_type_in_type : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context |