Merge PR#582: Fix warnings

4 files changed, 4 insertions, 7 deletions

diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 66bbf43f62..13e860a88a 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-
 (** The Coq toplevel loop. *)
 
 (** A buffer for the character read from a channel. We store the command
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9cf0750654..c3a7558609 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -292,7 +292,7 @@ let init_gc () =
     between coqtop and coqc. *)
 
 let usage () =
-  Envars.set_coqlib CErrors.error;
+  Envars.set_coqlib ~fail:CErrors.error;
   init_load_path ();
   if !batch_mode then Usage.print_usage_coqc ()
   else begin
@@ -609,7 +609,7 @@ let init_toplevel arglist =
       (* If we have been spawned by the Spawn module, this has to be done
        * early since the master waits us to connect back *)
       Spawned.init_channels ();
-      Envars.set_coqlib CErrors.error;
+      Envars.set_coqlib ~fail:CErrors.error;
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
       if !print_config then (Usage.print_config (); exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 66f782ffbe..e457ca61d0 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -83,7 +83,7 @@ let print_usage_channel co command =
 \n  -m, --memory           display total heap size at program exit\
 \n                         (use environment variable\
 \n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
-\n                          for full Gc stats dump)
+\n                          for full Gc stats dump)\
 \n  -native-compiler       precompile files for the native_compute machinery\
 \n  -h, -help, --help      print this list of options\
 \n";
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9ff320ee80..9f6f77ef1d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -41,7 +41,6 @@ let vernac_echo loc in_chan = let open Loc in
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
-let chan_beautify = ref stdout
 let beautify_suffix = ".beautified"
 
 let set_formatter_translator ch =
@@ -125,7 +124,7 @@ let rec interp_vernac sid (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely sid f
     | v ->
-      let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
+      let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
 
       (* Main STM interaction *)
       if ntip <> `NewTip then