diff options
| -rw-r--r-- | kernel/safe_typing.ml | 19 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 | ||||
| -rw-r--r-- | library/global.ml | 5 | ||||
| -rw-r--r-- | library/global.mli | 6 | ||||
| -rw-r--r-- | tactics/declare.ml | 7 |
5 files changed, 24 insertions, 19 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/library/global.ml b/library/global.ml index c4685370d1..24cfc57f28 100644 --- a/library/global.ml +++ b/library/global.ml @@ -102,8 +102,8 @@ let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) -let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) +let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) +let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) @@ -111,6 +111,7 @@ let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) let open_section () = globalize0 Safe_typing.open_section let close_section fs = globalize0_with_summary fs Safe_typing.close_section +let sections_are_opened () = Safe_typing.sections_are_opened (safe_env()) let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) diff --git a/library/global.mli b/library/global.mli index c45bf65d84..d689771f0a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,12 +46,12 @@ val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit val push_section_context : (Name.t array * Univ.UContext.t) -> unit -val export_private_constants : in_section:bool -> +val export_private_constants : Safe_typing.private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a + side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -80,6 +80,8 @@ val close_section : Summary.frozen -> unit (** Close the section and reset the global state to the one at the time when the section what opened. *) +val sections_are_opened : unit -> bool + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t diff --git a/tactics/declare.ml b/tactics/declare.ml index 3590146dfb..c7c0766587 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -249,14 +249,13 @@ let is_unsafe_typing_flags () = let define_constant ~side_effect ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) - let in_section = Lib.sections_are_opened () in let export, decl, unsafe = match cd with | DefinitionEntry de -> (* We deal with side effects *) if not de.proof_entry_opaque then (* This globally defines the side-effects in the environment. *) let body, eff = Future.force de.proof_entry_body in - let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in + let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = Entries.DefinitionEntry (cast_proof_entry de) in @@ -272,7 +271,7 @@ let define_constant ~side_effect ~name cd = | PrimitiveEntry e -> [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false in - let kn, eff = Global.add_constant ~side_effect ~in_section name decl in + let kn, eff = Global.add_constant ~side_effect name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); kn, eff, export @@ -319,7 +318,7 @@ let declare_variable ~name ~kind d = (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) let (body, eff) = Future.force de.proof_entry_body in - let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in + let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in let eff = get_roles export eff in let () = List.iter register_side_effect eff in let poly, univs = match de.proof_entry_universes with |