diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 4 |
4 files changed, 0 insertions, 14 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8fe27b3b97..ba6d4b05b3 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 962bb4302b..d596e36f34 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 fe853c093d..bfab447706 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 77c4f44e12..bccf560e16 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 |