diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 04ae5a454..baa983788 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -21,6 +21,14 @@ open Nametab functions of [Declare]; they return an absolute reference to the defined object *) +val constant_entry_of_com : + Coqast.t * Coqast.t option * bool -> Safe_typing.constant_entry + +val declare_global_definition : + Names.identifier -> + Safe_typing.constant_entry -> + Declare.strength -> bool -> Nametab.global_reference + val definition_body : identifier -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference |