diff options
Diffstat (limited to 'interp/declare.mli')
| -rw-r--r-- | interp/declare.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/interp/declare.mli b/interp/declare.mli index 6a09434645..ccd7d28bb5 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -69,11 +69,6 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool -(** Hooks for XML output *) -val xml_declare_variable : (object_name -> unit) Hook.t -val xml_declare_constant : (internal_flag * constant -> unit) Hook.t -val xml_declare_inductive : (bool * object_name -> unit) Hook.t - (** Declaration messages *) val definition_message : Id.t -> unit |