From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 01:13:59 +0200 Subject: Option -type-in-type: added support in checker and making it contaminating in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk? --- library/global.ml | 1 - library/global.mli | 1 - 2 files changed, 2 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 49fa2ef28..0419799b6 100644 --- a/library/global.ml +++ b/library/global.ml @@ -84,7 +84,6 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) -let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index 75a1ebee9..363bb5789 100644 --- a/library/global.mli +++ b/library/global.mli @@ -27,7 +27,6 @@ val named_context : unit -> Context.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit -val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) -- cgit v1.2.3