diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/library/declare.ml b/library/declare.ml index aa10cf3143..7364031d52 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -180,6 +180,17 @@ let declare_constant ?(internal = UserVerbose) id (cd,kind) = !xml_declare_constant (internal,kn); kn +let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition) + id ?types body = + let cb = + { Entries.const_entry_body = body; + const_entry_type = types; + const_entry_opaque = opaque; + const_entry_secctx = None } + in + declare_constant ~internal id + (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) + (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = |