2 files changed, 1 insertions, 19 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 70f422b514..7fcb38296f 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -32,14 +32,6 @@ type internal_flag =
   | InternalTacticRequest  (* kernel action, no message is displayed *)
   | UserIndividualRequest   (* user action, a message is displayed *)
 
-(** XML output hooks *)
-
-let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
-let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
-let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
@@ -95,7 +87,6 @@ let declare_variable id obj =
   declare_var_implicits id;
   Notation.declare_ref_arguments_scope (VarRef id);
   Heads.declare_head (EvalVarRef id);
-  if_xml (Hook.get f_xml_declare_variable) oname;
   oname
 
 
@@ -256,7 +247,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
     let id = Label.to_id (pi3 (Constant.repr3 c)) in
     ignore(add_leaf id o);
     update_tables c;
-    let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
     match role with
     | Safe_typing.Subproof -> ()
     | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
@@ -268,9 +258,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
     cst_kind = kind;
     cst_locl = local;
   } in
-  let kn = declare_constant_common id cst in
-  let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
-  kn
+  declare_constant_common id cst
 
 let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
@@ -410,7 +398,6 @@ let declare_mind mie =
   let isrecord,isprim = declare_projections mind in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
-  if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
   oname, isprim
 
 (* Declaration messages *)
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