Warning are enabled by default in interactive mode.

1 files changed, 10 insertions, 4 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 81e04525c..b706a81e6 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