From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jun 2016 18:25:02 +0200 Subject: Moving the typing_flags to the environment. --- library/declare.ml | 22 +++++++++++----------- library/declare.mli | 2 -- library/global.ml | 5 +++-- library/global.mli | 5 +++-- 4 files changed, 17 insertions(+), 17 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 335263f8f..4e9e68dff 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -58,11 +58,11 @@ let cache_variable ((sp,_),o) = let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ~flags:Declareops.safe_flags ((id,ty,poly),ctx) in + let () = Global.push_named_assum ((id,ty,poly),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let univs = Global.push_named_def ~flags:Declareops.safe_flags (id,de) in + let univs = Global.push_named_def (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); @@ -180,7 +180,7 @@ let discharge_constant ((sp, kn), obj) = (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry - (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), Declareops.safe_flags) + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -205,7 +205,7 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f -let declare_constant_common ~flags id cst = +let declare_constant_common id cst = let update_tables c = (* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) declare_constant_implicits c; @@ -216,7 +216,7 @@ let declare_constant_common ~flags id cst = List.iter (fun (c,ce,role) -> (* handling of private_constants just exported *) let o = inConstant { - cst_decl = ConstantEntry (false, ce, flags); + cst_decl = ConstantEntry (false, ce); cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; @@ -246,7 +246,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let export = (* We deal with side effects *) match cd with | DefinitionEntry de when @@ -259,24 +259,24 @@ let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualR | _ -> false in let cst = { - cst_decl = ConstantEntry (export,cd,flags); + cst_decl = ConstantEntry (export,cd); cst_hyps = [] ; cst_kind = kind; cst_locl = local; cst_exported = []; cst_was_seff = false; } in - let kn = declare_constant_common id cst ~flags in + let kn = declare_constant_common id cst in let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn -let declare_definition ?flags ?(internal=UserIndividualRequest) +let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in - declare_constant ?flags ~internal ~local id + declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of inductive blocks *) @@ -374,7 +374,7 @@ let declare_projections mind = Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant ~flags:Declareops.safe_flags id (ProjectionEntry entry, + let kn' = declare_constant id (ProjectionEntry entry, IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true,true diff --git a/library/declare.mli b/library/declare.mli index 41221d5c9..8dd24d278 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -54,11 +54,9 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry val declare_constant : - ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *) ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : - ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *) ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant diff --git a/library/global.ml b/library/global.ml index e456841f8..c53611931 100644 --- a/library/global.ml +++ b/library/global.ml @@ -77,13 +77,14 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a) -let push_named_def ~flags d = globalize (Safe_typing.push_named_def ~flags d) +let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) +let push_named_def d = globalize (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) 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 91fc55918..247ca20b4 100644 --- a/library/global.mli +++ b/library/global.mli @@ -27,11 +27,12 @@ val named_context : unit -> Context.Named.t (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit +val set_typing_flags : Declarations.typing_flags -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : flags:Declarations.typing_flags -> (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : flags:Declarations.typing_flags -> (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set +val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> -- cgit v1.2.3