From 5b9e2af49194adba609a748bb8ac03016fec4b07 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 23 Jun 2015 14:56:07 +0200
Subject: Warning are enabled by default in interactive mode.

---
 toplevel/coqtop.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 81e04525c8..b706a81e62 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -117,10 +117,15 @@ let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
 
 let set_batch_mode () = batch_mode := true
 
-let set_warning = function
-| "all" -> make_warn true
-| "none" -> make_warn false
-| _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
+let user_warning = ref false
+(** User explicitly set warning *)
+
+let set_warning p =
+  let () = user_warning := true in
+  match p with
+  | "all" -> make_warn true
+  | "none" -> make_warn false
+  | _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
 
 let toplevel_default_name = DirPath.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
@@ -636,6 +641,7 @@ let start () =
   let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
   (* In batch mode, Coqtop has already exited at this point. In interactive one,
      dump glob is nothing but garbage ...  *)
+  if not !user_warning then make_warn true;
   !toploop_run ();
   exit 1
 
-- 
cgit v1.2.3