[flags] Remove XML output flag.

This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.

It is also not included in the API, so it should either be included in
it or this PR be applied.

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