Some common points between coqc and other coq binaries.

- Binding coqc execution to the generic support for Coq binaries
  (i.e. to start_coq).
- Moving init_toploop to the init part of coq executables so that coqc
  can avoid to call it. By the way, it is unclear what workerloop
  should do with it. Also, it is unclear how much the -l option should
  be considered an coqidetop or coq*worker option. In any case, it
  should be disallowed in coqc, I guess?
- Moving the custom init part at the end of the initialization
  phase. Seems ok, despites the few involved side effects.

1 files changed, 5 insertions, 4 deletions

diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index c2bd8213b0..0087e4833c 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -14,11 +14,12 @@ let rec parse = function
   | [] -> []
 
 let worker_parse_extra ~opts extra_args =
-  Coqtop.Interactive, parse extra_args
+  (), parse extra_args
 
-let worker_init init ~opts =
+let worker_init init () ~opts =
   Flags.quiet := true;
-  init ()
+  init ();
+  Coqtop.init_toploop opts
 
 let start ~init ~loop =
   let open Coqtop in
@@ -27,6 +28,6 @@ let start ~init ~loop =
     help = (fun _ -> output_string stderr "Same options as coqtop");
     opts = Coqargs.default;
     init = worker_init init;
-    run = (fun ~opts:_ ~state:_ -> loop ());
+    run = (fun () ~opts:_ _state (* why is state not used *) -> loop ());
   } in
   start_coq custom