From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/declarations.mli | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) (limited to 'kernel/declarations.mli') diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 27c1c3f3..dc5c17a7 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -14,7 +14,10 @@ open Context declarations. This includes global constants/axioms, mutual inductive definitions, modules and module types *) -type engagement = ImpredicativeSet +type set_predicativity = ImpredicativeSet | PredicativeSet +type type_hierarchy = TypeInType | StratifiedType + +type engagement = set_predicativity * type_hierarchy (** {6 Representation of constants (Definition/Axiom) } *) @@ -76,12 +79,6 @@ type constant_body = { const_proj : projection_body option; const_inline_code : bool } -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] - -type side_effect = - | SEsubproof of constant * constant_body * seff_env - | SEscheme of (inductive * constant * constant_body * seff_env) list * string - (** {6 Representation of mutual inductive types in the kernel } *) type recarg = @@ -142,12 +139,10 @@ type one_inductive_body = { mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) mind_consnrealargs : int array; - (** Number of expected proper arguments of the constructors (w/o params) - (not used in the kernel) *) + (** Number of expected proper arguments of the constructors (w/o params) *) mind_consnrealdecls : int array; - (** Length of the signature of the constructors (with let, w/o params) - (not used in the kernel) *) + (** Length of the signature of the constructors (with let, w/o params) *) mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) @@ -245,8 +240,8 @@ and module_body = mod_type : module_signature; (** expanded type *) (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; - (** set of all constraints in the module *) - mod_constraints : Univ.constraints; + (** set of all universes constraints in the module *) + mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : Mod_subst.delta_resolver; mod_retroknowledge : Retroknowledge.action list } -- cgit v1.2.3