diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.ml | 2 | ||||
| -rw-r--r-- | library/declare.ml | 18 | ||||
| -rw-r--r-- | library/declare.mli | 4 | ||||
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 4 |
5 files changed, 16 insertions, 16 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index 463527820..f374f6dbe 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -227,7 +227,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = | ConstRef kn -> let cb = lookup_constant kn in let accu = - if cb.const_checked_guarded then accu + if cb.const_typing_flags.check_guarded then accu else ContextObjectMap.add (Axiom (Guarded kn)) Constr.mkProp accu in if not (Declareops.constant_has_body cb) then diff --git a/library/declare.ml b/library/declare.ml index 4be13109a..c49284bbc 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -50,11 +50,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 ~chkguard:true ((id,ty),ctx) in + let () = Global.push_named_assum ~flags:{check_guarded=true} ((id,ty),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let () = Global.push_named_def ~chkguard:true (id,de) in + let () = Global.push_named_def ~flags:{check_guarded=true} (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, (Univ.ContextSet.of_context de.const_entry_universes) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); @@ -156,7 +156,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 (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true) + ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), {check_guarded=true}) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -232,7 +232,7 @@ let declare_sideff env fix_exn se = const_entry_feedback = None; const_entry_polymorphic = cb.const_polymorphic; const_entry_universes = univs; - }, true); + }, {check_guarded=true}); cst_hyps = [] ; cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; cst_locl = true; @@ -253,7 +253,7 @@ let declare_sideff env fix_exn se = if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) -let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(flags={check_guarded=true}) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = let cd = (* We deal with side effects *) match cd with | Entries.DefinitionEntry de -> @@ -275,7 +275,7 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) | _ -> cd in let cst = { - cst_decl = ConstantEntry (cd,chkguard); + cst_decl = ConstantEntry (cd,flags); cst_hyps = [] ; cst_kind = kind; cst_locl = local; @@ -283,13 +283,13 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) let kn = declare_constant_common id cst in kn -let declare_definition ?chkguard ?(internal=UserVerbose) +let declare_definition ?flags ?(internal=UserVerbose) ?(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 ?chkguard ~internal ~local id + declare_constant ?flags ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of inductive blocks *) @@ -387,7 +387,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 ~chkguard:true id (ProjectionEntry entry, + let kn' = declare_constant ~flags:{check_guarded=true} id (ProjectionEntry entry, IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true diff --git a/library/declare.mli b/library/declare.mli index 94cebe3bd..cda8855d2 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -53,11 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> constr -> definition_entry val declare_constant : - ?chkguard:bool -> (** default [true] (check guardedness) *) + ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : - ?chkguard:bool -> (** default [true] (check guardedness) *) + ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) ?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 27f7f5266..ab326e37d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -77,8 +77,8 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a) -let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d) +let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a) +let push_named_def ~flags d = globalize0 (Safe_typing.push_named_def ~flags d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) diff --git a/library/global.mli b/library/global.mli index 388fee527..f7306fe57 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,9 +32,9 @@ val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : - chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit + flags:Declarations.typing_flags -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit val push_named_def : - chkguard:bool -> (Id.t * Entries.definition_entry) -> unit + flags:Declarations.typing_flags -> (Id.t * Entries.definition_entry) -> unit val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant |