diff options
author | 2016-06-16 17:47:44 +0200 | |
---|---|---|
committer | 2016-06-16 17:57:20 +0200 | |
commit | 0e2189a7a070dd356d5e549392d35d9d07b05058 (patch) | |
tree | 010ef6230603cb3beb91e9058fe0e1adb733c5d6 /library | |
parent | b857552b6ffd5e72b5124aee9e35fc5c14607173 (diff) |
Factorizing the uses of Declareops.safe_flags.
This allows a smooth addition of various unsafe flags without wreaking
havoc in the ML codebase.
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.ml | 10 | ||||
-rw-r--r-- | library/declare.mli | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/library/declare.ml b/library/declare.ml index 9ec299bed..335263f8f 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:{check_guarded=true} ((id,ty,poly),ctx) in + let () = Global.push_named_assum ~flags:Declareops.safe_flags ((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:{check_guarded=true} (id,de) in + let univs = Global.push_named_def ~flags:Declareops.safe_flags (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), {check_guarded=true}) + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), Declareops.safe_flags) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -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={check_guarded=true}) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let export = (* We deal with side effects *) match cd with | DefinitionEntry de when @@ -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:{check_guarded=true} id (ProjectionEntry entry, + let kn' = declare_constant ~flags:Declareops.safe_flags 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 3ba63b5a6..41221d5c9 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -54,11 +54,11 @@ 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 [check_guarded=true] *) + ?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 [check_guarded=true] *) + ?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 |