diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.ml | 18 | ||||
-rw-r--r-- | library/declare.mli | 2 | ||||
-rw-r--r-- | library/global.ml | 4 | ||||
-rw-r--r-- | library/global.mli | 6 |
4 files changed, 17 insertions, 13 deletions
diff --git a/library/declare.ml b/library/declare.ml index 02e6dadde..4be13109a 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 ((id,ty),ctx) in + let () = Global.push_named_assum ~chkguard: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 (id,de) in + let () = Global.push_named_def ~chkguard: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)) + ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), 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); 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 ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(chkguard=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 ?(internal = UserVerbose) ?(local = false) id ?(export_seff | _ -> cd in let cst = { - cst_decl = ConstantEntry cd; + cst_decl = ConstantEntry (cd,chkguard); cst_hyps = [] ; cst_kind = kind; cst_locl = local; @@ -283,13 +283,13 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff let kn = declare_constant_common id cst in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?chkguard ?(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 ~internal ~local id + declare_constant ?chkguard ~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 id (ProjectionEntry entry, + let kn' = declare_constant ~chkguard: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 d8a00db0c..94cebe3bd 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -53,9 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> constr -> definition_entry val declare_constant : + ?chkguard:bool -> (** default [true] (check guardedness) *) ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : + ?chkguard:bool -> (** default [true] (check guardedness) *) ?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 49fa2ef28..27f7f5266 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 a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize0 (Safe_typing.push_named_def d) +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 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 248e1f86d..388fee527 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,8 +31,10 @@ val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> unit +val push_named_assum : + chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit +val push_named_def : + chkguard:bool -> (Id.t * Entries.definition_entry) -> unit val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant |