[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.

24 files changed, 9 insertions, 120 deletions

diff --git a/Makefile.build b/Makefile.build
index b45c6427a..1c31f6c81 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -46,9 +46,6 @@ NO_RECALC_DEPS ?=
 # Non-empty runs the checker on all produced .vo files:
 VALIDATE ?=
 
-# Is "-xml" when building XML library:
-COQ_XML ?=
-
 # Output file names for timed builds
 TIME_OF_BUILD_FILE               ?= time-of-build.log
 TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
@@ -189,7 +186,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 # the output format of the unix command time. For instance:
 #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
+COQOPTS=$(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
 
 LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
@@ -273,9 +270,6 @@ $(error This Makefile needs GNU Make 3.81 or later (that is a version that suppo
 endif
 
 VO_TOOLS_DEP := $(COQTOPBEST)
-ifdef COQ_XML
- VO_TOOLS_DEP += $(COQDOC)
-endif
 ifdef VALIDATE
  VO_TOOLS_DEP += $(CHICKEN)
 endif
@@ -707,9 +701,9 @@ TIMING_EXTRA =
 endif
 
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
-	$(SHOW)'COQC $(COQ_XML) -noinit $<'
+	$(SHOW)'COQC -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA)
+	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA)
 
 # MExtraction.v generates the ml core file of the micromega tactic.
 # We check that this generated code is still in sync with the version
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index ed1d336d9..3ee65d6f2 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -614,7 +614,7 @@ is compiled by a Makefile with the following constraints:
 \begin{itemize}
 \item compilation is achieved by invoking make without specifying a target
 \item options are passed to Coq with make variable COQFLAGS that
-  includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML.
+  includes variables OPT, COQLIBS, and OTHERFLAGS.
 \end{itemize}
 These constraints are met by the makefiles produced by {\tt coq\_makefile}
 
diff --git a/interp/declare.ml b/interp/declare.ml
index 70f422b51..7fcb38296 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 6a0943464..ccd7d28bb 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
diff --git a/lib/flags.ml b/lib/flags.ml
index 0bce22f58..40bad9035 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -87,8 +87,6 @@ let in_toplevel = ref false
 
 let profile = false
 
-let xml_export = ref false
-
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
@@ -96,7 +94,6 @@ let time = ref false
 
 let raw_print = ref false
 
-
 let univ_print = ref false
 
 let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index eb4c37a54..388a3ff55 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -56,11 +56,6 @@ val stm_debug : bool ref
 
 val profile : bool
 
-(* Legacy flags *)
-
-(* -xml option: xml hooks will be called *)
-val xml_export : bool ref
-
 (* -ide_slave: printing will be more verbose, will affect stm caching *)
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
diff --git a/library/declaremods.ml b/library/declaremods.ml
index e7aa5bd0d..6d9295bde 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -557,17 +557,6 @@ let openmodtype_info =
   Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO"
 
 
-(** XML output hooks *)
-
-let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore ()
-let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore ()
-let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore ()
-let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore ()
-let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore ()
-let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
 (** {6 Modules : start, end, declare} *)
 
 module RawModOps = struct
@@ -589,7 +578,6 @@ let start_module interp_modast export id args res fs =
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-  if_xml (Hook.get f_xml_start_module) mp;
   mp
 
 let end_module () =
@@ -628,7 +616,6 @@ let end_module () =
   assert (eq_full_path (fst newoname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
 
-  if_xml (Hook.get f_xml_end_module) mp;
   mp
 
 let declare_module interp_modast id args res mexpr_o fs =
@@ -682,7 +669,6 @@ let declare_module interp_modast id args res mexpr_o fs =
 
   let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
   ignore (Lib.add_leaf id (in_module sobjs));
-  if_xml (Hook.get f_xml_declare_module) mp;
   mp
 
 end
@@ -699,7 +685,6 @@ let start_modtype interp_modast id args mtys fs =
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
-  if_xml (Hook.get f_xml_start_module_type) mp;
   mp
 
 let end_modtype () =
@@ -716,7 +701,6 @@ let end_modtype () =
   assert (eq_full_path (fst oname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd oname)) mp);
 
-  if_xml (Hook.get f_xml_end_module_type) mp;
   mp
 
 let declare_modtype interp_modast id args mtys (mty,ann) fs =
@@ -750,7 +734,6 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   check_subtypes_mt mp sub_mty_l;
 
   ignore (Lib.add_leaf id (in_modtype sobjs));
-  if_xml (Hook.get f_xml_declare_module_type) mp;
   mp
 
 end
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 005594b8d..9d750b616 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -63,14 +63,6 @@ val start_modtype :
 
 val end_modtype : unit -> module_path
 
-(** Hooks for XML output *)
-val xml_declare_module : (module_path -> unit) Hook.t
-val xml_start_module : (module_path -> unit) Hook.t
-val xml_end_module : (module_path -> unit) Hook.t
-val xml_declare_module_type : (module_path -> unit) Hook.t
-val xml_start_module_type : (module_path -> unit) Hook.t
-val xml_end_module_type : (module_path -> unit) Hook.t
-
 (** {6 Libraries i.e. modules on disk } *)
 
 type library_name = DirPath.t
diff --git a/library/lib.ml b/library/lib.ml
index a24d20c68..c6a0253b3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -512,11 +512,6 @@ let is_in_section ref =
 
 (*************)
 (* Sections. *)
-
-(* XML output hooks *)
-let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
-let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
-
 let open_section id =
   let olddir,(mp,oldsec) = !lib_state.path_prefix in
   let dir = add_dirpath_suffix olddir id in
@@ -528,7 +523,6 @@ let open_section id =
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
   lib_state := { !lib_state with path_prefix = prefix };
-  if !Flags.xml_export then Hook.get f_xml_open_section id;
   add_section ()
 
 
@@ -556,7 +550,6 @@ let close_section () =
   let full_olddir = fst !lib_state.path_prefix in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
-  if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
diff --git a/library/lib.mli b/library/lib.mli
index f1c9bfca2..3dcec1d53 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -150,10 +150,6 @@ val unfreeze : frozen -> unit
 
 val init : unit -> unit
 
-(** XML output hooks *)
-val xml_open_section : (Names.Id.t -> unit) Hook.t
-val xml_close_section : (Names.Id.t -> unit) Hook.t
-
 (** {6 Section management for discharge } *)
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 type variable_context = variable_info list 
@@ -165,7 +161,7 @@ val named_of_variable_context : variable_context -> Context.Named.t
 val section_segment_of_constant : Names.constant -> abstr_info
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
 val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
-                                                                                                     
+
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
diff --git a/library/library.ml b/library/library.ml
index 20ecc2c22..28afa054e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -551,8 +551,6 @@ let in_require : require_obj -> obj =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
-let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
-
 let warn_require_in_module =
   CWarnings.create ~name:"require-in-module" ~category:"deprecated"
                    (fun () -> strbrk "Require inside a module is" ++
@@ -574,7 +572,6 @@ let require_library_from_dirpath modrefl export =
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
-    if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
   ()
 
 (* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mli b/library/library.mli
index 604167804..6c624ce52 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -67,9 +67,6 @@ val library_full_filename : DirPath.t -> string
   (** - Overwrite the filename of all libraries (used when restoring a state) *)
 val overwrite_library_filenames : string -> unit
 
-(** {6 Hook for the xml exportation of libraries } *)
-val xml_require : (DirPath.t -> unit) Hook.t
-
 (** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
 exception LibNotFound
diff --git a/man/coqide.1 b/man/coqide.1
index f82bf2ad4..3592f6e4e 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -123,13 +123,6 @@ Set sort Set impredicative.
 .TP
 .B \-dont\-load\-proofs
 Don't load opaque proofs in memory.
-.TP
-.B \-xml
-Export XML files either to the hierarchy rooted in
-the directory
-.B COQ_XML_LIBRARY_ROOT
-(if set) or to stdout (if unset).
-
 
 .SH SEE ALSO
 
diff --git a/man/coqtop.1 b/man/coqtop.1
index feee7fd8b..62d17aa67 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -153,12 +153,6 @@ set sort Set impredicative
 .B \-dont\-load\-proofs
 don't load opaque proofs in memory
 
-.TP
-.B \-xml
-export XML files either to the hierarchy rooted in
-the directory $COQ_XML_LIBRARY_ROOT (if set) or to
-stdout (if unset)
-
 .SH SEE ALSO
 
 .BR coqc (1),
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 5fcbb43b6..636027f9b 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -368,9 +368,6 @@ let rec string loc ~comm_level bp len = parser
      let loc = set_loc_pos loc bp ep in
      err loc Unterminated_string
 
-(* Hook for exporting comment into xml theory files *)
-let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
-
 (* To associate locations to a file name *)
 let current_file = ref None
 
@@ -432,9 +429,6 @@ let null_comment s =
 
 let comment_stop ep =
   let current_s = Buffer.contents current_comment in
-  if !Flags.xml_export && Buffer.length current_comment > 0 &&
-    (!between_commands || not(null_comment current_s)) then
-      Hook.get f_xml_output_comment current_s;
   (if !Flags.beautify && Buffer.length current_comment > 0 &&
     (!between_commands || not(null_comment current_s)) then
     let bp = match !comment_begin with
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 09c9d8ee4..77d652b18 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -19,9 +19,6 @@ val get_keyword_state : unit -> keyword_state
 val check_ident : string -> unit
 val is_ident : string -> bool
 val check_keyword : string -> unit
-
-val xml_output_comment : (string -> unit) Hook.t
-
 val terminal : string -> Tok.t
 
 (** The lexer of Coq: *)
diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
index 39a7103d1..40abb215e 100644
--- a/test-suite/bugs/closed/HoTT_coq_032.v
+++ b/test-suite/bugs/closed/HoTT_coq_032.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; coq-prog-args: ("-xml") -*- *)
 Set Implicit Arguments.
 Generalizable All Variables.
 Set Asymmetric Patterns.
diff --git a/tools/beautify-archive b/tools/beautify-archive
index 6bfa974a5..a327ea44e 100755
--- a/tools/beautify-archive
+++ b/tools/beautify-archive
@@ -23,7 +23,7 @@ cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE
 cd $NEWARCHIVE
 rm description || true
 make clean
-make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS)' || \
  { echo ---- Failed to beautify; exit 1; }
 echo -------- Upgrading files in the beautification directory --------------
 beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX`
diff --git a/tools/check-translate b/tools/check-translate
index 3dd824053..acb6f4590 100755
--- a/tools/check-translate
+++ b/tools/check-translate
@@ -2,7 +2,7 @@
 
 echo -------------- Producing translated files ---------------------
 rm */*/*.v8 >& /dev/null
-make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; }
+make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; }
 if [ -e translated ]; then rm -r translated; fi
 if [ -e successful-translation ]; then rm -r successful-translation; fi
 if [ -e failed-translation ]; then rm -r failed-translation; fi
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 4595af6e8..862225d3d 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -94,7 +94,7 @@ let parse_args () =
     | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet"
-      |"-silent"|"-m"|"-xml"|"-beautify"|"-strict-implicit"
+      |"-silent"|"-m"|"-beautify"|"-strict-implicit"
       |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8fe27b3b9..ba6d4b05b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -585,7 +585,6 @@ let parse_args arglist =
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ())
     |"-where" -> print_where := true
-    |"-xml" -> Flags.xml_export := true
 
     (* Unknown option *)
     | s -> extras := s :: !extras
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 962bb4302..d596e36f3 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -78,9 +78,6 @@ let print_usage_channel co command =
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
-\n  -xml                   export XML files either to the hierarchy rooted in\
-\n                         the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
-\n                         stdout (if unset)\
 \n  -time                  display the time taken by each command\
 \n  -profile-ltac          display the time taken by each (sub)tactic\
 \n  -m, --memory           display total heap size at program exit\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index fe853c093..bfab44770 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -243,10 +243,6 @@ let process_expr sid loc_ast =
   checknav_deep loc_ast;
   interp_vernac sid loc_ast
 
-(* XML output hooks *)
-let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
-let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
-
 let warn_file_no_extension =
   CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
          (fun (f,ext) ->
@@ -308,7 +304,6 @@ let compile verbosely f =
         ~v_file:long_f_dot_v);
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
-      if !Flags.xml_export then Hook.get f_xml_start_library ();
       let wall_clock1 = Unix.gettimeofday () in
       let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
       Stm.join ();
@@ -318,7 +313,6 @@ let compile verbosely f =
       Aux_file.record_in_aux_at "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
-      if !Flags.xml_export then Hook.get f_xml_end_library ();
       Dumpglob.end_dump_glob ()
   | BuildVio ->
       let long_f_dot_v = ensure_v f in
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 77c4f44e1..bccf560e1 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -21,7 +21,3 @@ val load_vernac : bool -> Stateid.t -> string -> Stateid.t
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)
 val compile : bool -> string -> unit
-
-(** Set XML hooks *)
-val xml_start_library : (unit -> unit) Hook.t
-val xml_end_library   : (unit -> unit) Hook.t