diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 20 | ||||
| -rw-r--r-- | toplevel/usage.ml | 5 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 4 |
4 files changed, 2 insertions, 33 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5ecd71a39..0f8524e92 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -138,8 +138,6 @@ let set_toplevel_name dir = if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); toplevel_name := dir -let remove_top_ml () = Mltop.remove () - let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> strbrk "The inputstate option is deprecated and discouraged.") @@ -585,24 +583,8 @@ let parse_args arglist = |"-type-in-type" -> set_type_in_type () |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) - |"--print-version" -> Usage.machine_readable_version (exitcode ()) + |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-where" -> print_where := true - |"-xml" -> Flags.xml_export := true - - (* Deprecated options *) - |"-byte" -> warning "option -byte deprecated, call with .byte suffix" - |"-opt" -> warning "option -opt deprecated, call with .opt suffix" - |"-full" -> warning "option -full deprecated" - |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml () - |"-emacs-U" -> - warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () - |"-v7" -> user_err Pp.(str "This version of Coq does not support v7 syntax") - |"-v8" -> warning "Obsolete option \"-v8\"." - |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"." - |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"." - |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"." - |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ()) - |"-quality" -> warning "Obsolete option \"-quality\"." (* Unknown option *) | s -> extras := s :: !extras diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f8c7b114c..d596e36f3 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -57,7 +57,7 @@ let print_usage_channel co command = \n -where print Coq's standard library location and exit\ \n -config, --config print Coq's configuration information and exit\ \n -v, --version print Coq version and exit\ -\n --print-version print Coq version in easy to parse format and exit\ +\n -print-version print Coq version in easy to parse format and exit\ \n -list-tags print highlight color tags known by Coq and exit\ \n\ \n -quiet unset display of extra information (implies -w \"-all\")\ @@ -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 |