A few fixes to the build system (mostly for ocamlbuild)

 * vars.mli was mentionning Term instead of Constr, leading to a dep cycle
 * Having a file named toplevel/toplevel.ml isn't a good idea when we also
   have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
   We rename toplevel.ml into Coqloop.ml
 * Extra cleanup of toplevel.mllib :
   - Ppextra isn't anywhere around (?!)
   - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
   - Vernacexpr is a .mli and shouldn't appear in an .mllib
 * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
 * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
   for coqchk).

5 files changed, 4 insertions, 8 deletions

diff --git a/toplevel/toplevel.ml b/toplevel/coqloop.ml
index 3bcf935ccb..3bcf935ccb 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/coqloop.ml
diff --git a/toplevel/toplevel.mli b/toplevel/coqloop.mli
index 1375f33619..1375f33619 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/coqloop.mli
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a0de42bf65..68f58e6662 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -401,7 +401,7 @@ let init arglist =
         if !batch_mode then mt ()
         else str "Error during initialization:" ++ fnl ()
       in
-      fatal_error (msg ++ Toplevel.print_toplevel_error any)
+      fatal_error (msg ++ Coqloop.print_toplevel_error any)
   end;
   if !batch_mode then begin
     flush_all();
@@ -425,7 +425,7 @@ let start () =
   else if !Flags.coq_slave_mode > 0 then
     Stm.slave_main_loop ()
   else
-    Toplevel.loop();
+    Coqloop.loop();
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
   Mltop.ocaml_toploop();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 73e2148494..ee511edbbc 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -9,7 +9,7 @@
 (** The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input
    state, load the files given on the command line, load the ressource file,
-   produce the output state if any, and finally will launch [Toplevel.loop]. *)
+   produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
 val init_toplevel : string list -> unit
 
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index ab8c896230..0ad82abd34 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -2,9 +2,6 @@ Himsg
 Cerrors
 Class
 Locality
-Vernacexpr
-Ppextra
-Ppvernac
 Metasyntax
 Auto_ind_decl
 Search
@@ -15,7 +12,6 @@ Obligations
 Command
 Classes
 Record
-Ppvernac
 Vernacinterp
 Mltop
 Vernacentries
@@ -24,7 +20,7 @@ Stm
 Whelp
 Vernac
 Ide_slave
-Toplevel
 Usage
+Coqloop
 Coqinit
 Coqtop