diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/library/declare.mli b/library/declare.mli index 3c04ddf57..3a7849232 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -92,13 +92,6 @@ val clear_proofs : named_context -> named_context val context_of_global_reference : global_reference -> section_context -(* Turn a global reference into a construction *) -val constr_of_reference : global_reference -> constr - -(* Turn a construction denoting a global into a reference; - raise [Not_found] if not a global *) -val reference_of_constr : constr -> global_reference - val global_qualified_reference : qualid -> constr val global_absolute_reference : section_path -> constr val global_reference_in_absolute_module : dir_path -> identifier -> constr @@ -120,6 +113,6 @@ val strength_of_global : global_reference -> strength val library_part : global_reference -> dir_path (* hooks for XML output *) -val set_xml_declare_variable : (kernel_name -> unit) -> unit -val set_xml_declare_constant : (kernel_name -> unit) -> unit -val set_xml_declare_inductive : (kernel_name -> unit) -> unit +val set_xml_declare_variable : (object_name -> unit) -> unit +val set_xml_declare_constant : (object_name -> unit) -> unit +val set_xml_declare_inductive : (object_name -> unit) -> unit |