diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 19 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 | ||||
| -rw-r--r-- | kernel/section.ml | 2 | ||||
| -rw-r--r-- | kernel/section.mli | 3 |
4 files changed, 19 insertions, 11 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9b4d2e69ac..fc55720583 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -173,6 +173,8 @@ let is_initial senv = | [], NONE -> ModPath.equal senv.modpath ModPath.initial | _ -> false +let sections_are_opened senv = not (Section.is_empty senv.sections) + let delta_of_senv senv = senv.modresolver,senv.paramresolver let constant_of_delta_kn_senv senv kn = @@ -587,10 +589,10 @@ type global_declaration = type exported_private_constant = Constant.t -let add_constant_aux ~in_section senv (kn, cb) = +let add_constant_aux senv (kn, cb) = let l = Constant.label kn in (* This is the only place where we hashcons the contents of a constant body *) - let cb = if in_section then cb else Declareops.hcons_const_body cb in + let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with | Undef (Some lev) -> @@ -799,7 +801,7 @@ let push_opaque_proof pf senv = let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in senv, o -let export_private_constants ~in_section ce senv = +let export_private_constants ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> @@ -815,10 +817,10 @@ let export_private_constants ~in_section ce senv = let senv, bodies = List.fold_left_map map senv exported in let exported = List.map (fun (kn, _) -> kn) exported in (* No delayed constants to declare *) - let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in + let senv = List.fold_left add_constant_aux senv bodies in (ce, exported), senv -let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = +let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = match decl with @@ -852,14 +854,14 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen | Undef _ | Def _ | Primitive _ as body -> senv, { cb with const_body = body }, [] in - let senv = add_constant_aux ~in_section senv (kn, cb) in + let senv = add_constant_aux senv (kn, cb) in add_constraints_list delayed_cst senv in let senv = match decl with | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> - if in_section then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); + if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in @@ -1001,12 +1003,11 @@ let close_section senv = in let fold senv = function | `Definition (kn, cb) -> - let in_section = not (Section.is_empty senv.sections) in let info = cooking_info (Section.segment_of_constant env0 kn sections0) in let r = { Cooking.from = cb; info } in let cb = Term_typing.translate_recipe senv.env kn r in (* Delayed constants are already in the global environment *) - add_constant_aux ~in_section senv (kn, cb) + add_constant_aux senv (kn, cb) | `Inductive (ind, mib) -> let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in let mie = Cooking.cook_inductive info mib in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index d97d61a72f..1b55293f1c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -82,13 +82,13 @@ type global_declaration = type exported_private_constant = Constant.t -val export_private_constants : in_section:bool -> +val export_private_constants : private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer (** returns the main constant plus a certificate of its validity *) val add_constant : - side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> + side_effect:'a effect_entry -> Label.t -> global_declaration -> (Constant.t * 'a) safe_transformer (** Adding an inductive type *) @@ -138,6 +138,8 @@ val open_section : safe_transformer0 val close_section : safe_transformer0 +val sections_are_opened : safe_environment -> bool + (** Insertion of local declarations (Local or Variables) *) val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 diff --git a/kernel/section.ml b/kernel/section.ml index babd9fe7a1..a1242f0faf 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -43,6 +43,8 @@ let empty = [] let is_empty = List.is_empty +let depth = List.length + let has_poly_univs = function | [] -> false | sec :: _ -> sec.has_poly_univs diff --git a/kernel/section.mli b/kernel/section.mli index 56b4d9ba8f..ec863b3b90 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -21,6 +21,9 @@ val empty : 'a t val is_empty : 'a t -> bool (** Checks whether there is no opened section *) +val depth : 'a t -> int +(** Number of nested sections (0 if no sections are open) *) + (** {6 Manipulating sections} *) type section_entry = |