1 files changed, 22 insertions, 29 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index eacd1dcf..01056b6a 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -10,8 +10,8 @@
 
 let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s))
 
-let fatal_error ?extra exn =
-  Topfmt.print_err_exn ?extra exn;
+let fatal_error exn =
+  Topfmt.print_err_exn Topfmt.ParsingCommandLine exn;
   let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
   exit exit_code
 
@@ -52,7 +52,6 @@ type coq_cmdopts = {
   compilation_mode : compilation_mode;
 
   toplevel_name : Names.DirPath.t;
-  toploop : string option;
 
   compile_list: (string * bool) list;  (* bool is verbosity  *)
   compilation_output_name : string option;
@@ -69,6 +68,7 @@ type coq_cmdopts = {
   impredicative_set : Declarations.set_predicativity;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
+  diffs_set   : bool;
   time        : bool;
 
   filter_opts : bool;
@@ -81,6 +81,8 @@ type coq_cmdopts = {
   print_config: bool;
   output_context : bool;
 
+  print_emacs : bool;
+
   inputstate  : string option;
   outputstate : string option;
 
@@ -100,7 +102,6 @@ let init_args = {
   compilation_mode = BuildVo;
 
   toplevel_name = Names.(DirPath.make [Id.of_string "Top"]);
-  toploop = None;
 
   compile_list = [];
   compilation_output_name = None;
@@ -117,6 +118,7 @@ let init_args = {
   impredicative_set = Declarations.PredicativeSet;
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
+  diffs_set    = false;
   time         = false;
 
   filter_opts  = false;
@@ -129,6 +131,8 @@ let init_args = {
   print_config = false;
   output_context = false;
 
+  print_emacs = false;
+
   inputstate  = None;
   outputstate = None;
 }
@@ -148,9 +152,9 @@ let add_vo_require opts d p export =
 
 let add_compat_require opts v =
   match v with
-  | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false)
   | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
-  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
+  | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
+  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
 
 let set_batch_mode opts =
   Flags.quiet := true;
@@ -191,11 +195,8 @@ let set_vio_checking_j opts opt j =
 
 (** Options for proof general *)
 let set_emacs opts =
-  if not (Option.is_empty opts.toploop) then
-    CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop");
-  Coqloop.print_emacs := true;
   Printer.enable_goal_tags_printing := true;
-  { opts with color = `OFF }
+  { opts with color = `OFF; print_emacs = true }
 
 let set_color opts = function
 | "yes" | "on" -> { opts with color = `ON }
@@ -310,12 +311,9 @@ let usage batch =
   let lp = Coqinit.toplevel_init_load_path () in
   (* Necessary for finding the toplevels below *)
   List.iter Mltop.add_coq_path lp;
-  if batch then Usage.print_usage_coqc ()
-  else begin
-    Mltop.load_ml_objects_raw_rex
-      (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
-    Usage.print_usage_coqtop ()
-  end
+  if batch
+  then Usage.print_usage_coqc ()
+  else Usage.print_usage_coqtop ()
 
 (* Main parsing routine *)
 let parse_args arglist : coq_cmdopts * string list =
@@ -401,7 +399,7 @@ let parse_args arglist : coq_cmdopts * string list =
       }}
 
     |"-async-proofs-worker-priority" ->
-      WorkerLoop.async_proofs_worker_priority := get_priority opt (next ());
+      CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ());
       oval
 
     |"-async-proofs-private-flags" ->
@@ -427,7 +425,7 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-worker-id" -> set_worker_id opt (next ()); oval
 
     |"-compat" ->
-      let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in
+      let v = G_vernac.parse_compat_version (next ()) in
       Flags.compat_version := v;
       add_compat_require oval v
 
@@ -500,11 +498,6 @@ let parse_args arglist : coq_cmdopts * string list =
       let oval = add_compile oval false (next ()) in
       { oval with compilation_mode = Vio2Vo }
 
-    |"-toploop" ->
-      if !Coqloop.print_emacs then
-        CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible");
-      { oval with toploop = Some (next ()) }
-
     |"-w" | "-W" ->
       let w = next () in
       if w = "none" then
@@ -535,15 +528,15 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> { oval with print_config = true }
     |"-debug" -> Coqinit.set_debug (); oval
+    |"-diffs" -> let opt = next () in
+                  if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then
+                    Proof_diffs.write_diffs_option opt
+                  else
+                    (prerr_endline ("Error: on|off|removed expected after -diffs"); exit 1);
+                  { oval with diffs_set = true }
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-filteropts" -> { oval with filter_opts = true }
-    |"-ideslave" ->
-      if !Coqloop.print_emacs then
-        CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible");
-      Flags.ide_slave := true;
-      { oval with toploop = Some "coqidetop" }
-
     |"-impredicative-set" ->
       { oval with impredicative_set = Declarations.ImpredicativeSet }
     |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval