A new infrastructure for warnings.

On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.

We also provide a vernacular Set Warnings which takes the same flags as argument.

Note that coqc now prints warnings.

The name and category of a warning are printed with the warning itself.

On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:

1) create it by:

let warn_my_warning =
  CWarnings.create ~name:"my-warning" ~category:"my-category"
    (fun args -> Pp.strbrk ...)

2) print it by:

warn_my_warning args

15 files changed, 181 insertions, 92 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0bb7966d7..e45ab4b4e 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -13,13 +13,6 @@ open Type_errors
 open Pretype_errors
 open Indrec
 
-let print_loc loc =
-  if Loc.is_ghost loc then
-    (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    (int (fst loc) ++ str"-" ++ int (snd loc))
-
 let guill s = str "\"" ++ str s ++ str "\""
 
 (** Invariant : exceptions embedded in EvaluatedError satisfy
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index cd6ccd565..a67c887af 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -9,10 +9,6 @@
 (** Toplevel Exception *)
 exception EvaluatedError of Pp.std_ppcmds * exn option
 
-(** Error report. *)
-
-val print_loc : Loc.t -> Pp.std_ppcmds
-
 (** Pre-explain a vernac interpretation error *)
 
 val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 10e9b30be..fa68a69fb 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -32,7 +32,6 @@ type coercion_error_kind =
   | NotAFunction
   | NoSource of cl_typ option
   | ForbiddenSourceClass of cl_typ
-  | NotUniform
   | NoTarget
   | WrongTarget of cl_typ * cl_typ
   | NotAClass of global_reference
@@ -51,9 +50,6 @@ let explain_coercion_error g = function
       (str ": cannot find the source class of " ++ Printer.pr_global g)
   | ForbiddenSourceClass cl ->
       pr_class cl ++ str " cannot be a source class"
-  | NotUniform ->
-      (Printer.pr_global g ++
-         str" does not respect the uniform inheritance condition");
   | NoTarget ->
       (str"Cannot find the target class")
   | WrongTarget (clt,cl) ->
@@ -247,6 +243,12 @@ booleen "coercion identite'?"
 lorque source est None alors target est None aussi.
 *)
 
+let warn_uniform_inheritance =
+  CWarnings.create ~name:"uniform-inheritance" ~category:"typechecker"
+         (fun g ->
+          Printer.pr_global g ++
+            strbrk" does not respect the uniform inheritance condition")
+
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
   let t = Global.type_of_global_unsafe coef in
@@ -262,7 +264,7 @@ let add_new_coercion_core coef stre poly source target isid =
   in
   check_source (Some cls);
   if not (uniform_cond (llp-ind) lvs) then
-    Feedback.msg_warning (explain_coercion_error coef NotUniform);
+    warn_uniform_inheritance coef;
   let clt =
     try
       get_target tg ind
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 28fa8a171..ffa2484ee 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -82,6 +82,12 @@ let red_constant_entry n ce sigma = function
       { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
         (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
 
+let warn_implicits_in_term =
+  CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
+         (fun () ->
+          strbrk "Implicit arguments declaration relies on type." ++ spc () ++
+            strbrk "The term declares more implicits than the type here.")
+        
 let interp_definition pl bl p red_option c ctypopt =
   let env = Global.env() in
   let ctx = Evd.make_evar_universe_context env pl in
@@ -119,9 +125,7 @@ let interp_definition pl bl p red_option c ctypopt =
           impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
-	then Feedback.msg_warning
-          (strbrk "Implicit arguments declaration relies on type." ++ spc () ++
-	   strbrk "The term declares more implicits than the type here.");
+	then warn_implicits_in_term ();
         let vars = Univ.LSet.union (Universes.universes_of_constr body) 
           (Universes.universes_of_constr typ) in
         let ctx = Evd.restrict_universe_context !evdref vars in
@@ -136,11 +140,15 @@ let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
   ce
 
+let warn_local_let_definition =
+  CWarnings.create ~name:"local-let-definition" ~category:"scope"
+         (fun id ->
+          pr_id id ++ strbrk " is declared as a local definition")
+
 let get_locality id = function
 | Discharge ->
   (** If a Let is defined outside a section, then we consider it as a local definition *)
-  let msg = pr_id id ++ strbrk " is declared as a local definition" in
-  let () = Feedback.msg_warning msg in
+   warn_local_let_definition id;
   true
 | Local -> true
 | Global -> false
@@ -158,6 +166,12 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
+let warn_definition_not_visible =
+  CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
+         (fun ident ->
+          strbrk "Section definition " ++
+            pr_id ident ++ strbrk " is not visible from current goals")
+
 let declare_definition ident (local, p, k) ce pl imps hook =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
@@ -169,9 +183,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
     let () = if Pfedit.refining () then
-      let msg = strbrk "Section definition " ++
-        pr_id ident ++ strbrk " is not visible from current goals" in
-      Feedback.msg_warning msg
+	       warn_definition_not_visible ident
     in
     gr
   | Discharge | Local | Global ->
@@ -217,7 +229,7 @@ match local with
   let () = assumption_message ident in
   let () =
     if is_verbose () && Pfedit.refining () then
-    Feedback.msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
+    Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
     strbrk " is not visible from current goals")
   in
   let r = VarRef ident in
@@ -780,20 +792,25 @@ let rec partial_order cmp = function
 let non_full_mutual_message x xge y yge isfix rest =
   let reason =
     if Id.List.mem x yge then
-      pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely"
+      pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely"
     else if Id.List.mem y xge then
-      pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely"
+      pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely"
     else
-      pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in
-  let e = if List.is_empty rest then reason else str "e.g., " ++ reason in
+      pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in
+  let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in
   let k = if isfix then "fixpoint" else "cofixpoint" in
   let w =
     if isfix
-    then str "Well-foundedness check may fail unexpectedly." ++ fnl()
+    then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl()
     else mt () in
-  str "Not a fully mutually defined " ++ str k ++ fnl () ++
+  strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++
   str "(" ++ e ++ str ")." ++ fnl () ++ w
 
+let warn_non_full_mutual =
+  CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints"
+         (fun (x,xge,y,yge,isfix,rest) ->
+          non_full_mutual_message x xge y yge isfix rest)
+
 let check_mutuality env isfix fixl =
   let names = List.map fst fixl in
   let preorder =
@@ -803,7 +820,7 @@ let check_mutuality env isfix fixl =
   let po = partial_order Id.equal preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
     | (x,Inr xge)::(y,Inr yge)::rest ->
-	Feedback.msg_warning (non_full_mutual_message x xge y yge isfix rest)
+       warn_non_full_mutual (x,xge,y,yge,isfix,rest)
     | _ -> ()
 
 type structured_fixpoint_expr = {
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 65c5917b7..50a228050 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -135,6 +135,7 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    Feedback.msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
-    Flags.V8_2
-  | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".")
+    Errors.errorlabstrm "get_compat_version"
+      (str "Compatibility with version " ++ str s ++ str " not supported.")
+  | s -> Errors.errorlabstrm "get_compat_version"
+      (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 00e0219f1..67a5472d5 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -146,9 +146,8 @@ let print_highlight_location ib loc =
                       str sn ++ str dn) in
 	  (l1 ++ li ++ ln)
   in
-  let loc = Loc.make_loc (bp,ep) in
-  (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++
-     highlight_lines ++ fnl ())
+  let loc  = Loc.make_loc (bp,ep) in
+  (Pp.pr_loc loc ++ highlight_lines ++ fnl ())
 
 (* Functions to report located errors in a file. *)
 
@@ -163,10 +162,7 @@ let print_location_in_file loc =
     in
     let open Loc in
     hov 0 (* No line break so as to follow emacs error message format *)
-	(errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++
-	   str", line " ++ int loc.line_nb ++ str", characters " ++
-	   Cerrors.print_loc (Loc.make_loc (loc.bp-loc.bol_pos,loc.ep-loc.bol_pos))) ++ str":" ++
-      fnl ()
+	(errstrm ++ Pp.pr_loc loc)
 
 let valid_buffer_loc ib loc =
   not (Loc.is_ghost loc) &&
@@ -249,7 +245,7 @@ let print_toplevel_error (e, info) =
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   let fname = loc.Loc.fname in
   let locmsg =
-    if String.equal fname "" then
+    if Loc.is_ghost loc || String.equal fname "" then
       if locate_exn e && valid_buffer_loc top_buffer loc then
 	print_highlight_location top_buffer loc
       else mt ()
@@ -279,7 +275,9 @@ let rec discard_to_dot () =
     | e when Errors.noncritical e -> ()
 
 let read_sentence () =
-  try Vernac.parse_sentence (top_buffer.tokens, None)
+  try
+    let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
+    CWarnings.set_current_loc loc; r
   with reraise ->
     let reraise = Errors.push reraise in
     discard_to_dot ();
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e34f38eb3..93ed2481b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -123,16 +123,6 @@ let engage () =
 
 let set_batch_mode () = batch_mode := true
 
-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)
 let set_toplevel_name dir =
@@ -142,18 +132,27 @@ let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
 
+let warn_deprecated_inputstate =
+  CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
+         (fun () -> strbrk "The inputstate option is deprecated and discouraged.")
+
 let inputstate = ref ""
 let set_inputstate s =
-  let () = Feedback.msg_warning (str "The inputstate option is deprecated and discouraged.") in
+  warn_deprecated_inputstate ();
   inputstate:=s
 let inputstate () =
   if not (String.is_empty !inputstate) then
     let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
     intern_state fname
 
+let warn_deprecated_outputstate =
+  CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
+         (fun () ->
+          strbrk "The outputstate option is deprecated and discouraged.")
+
 let outputstate = ref ""
 let set_outputstate s =
-  let () = Feedback.msg_warning (str "The outputstate option is deprecated and discouraged.") in
+  warn_deprecated_outputstate ();
   outputstate:=s
 let outputstate () =
   if not (String.is_empty !outputstate) then
@@ -532,7 +531,7 @@ let parse_args arglist =
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> set_toploop (next ())
-    |"-w" -> set_warning (next ())
+    |"-w" | "-W" -> CWarnings.set_flags (next ())
     |"-o" -> Flags.compilation_output_name := Some (next())
 
     (* Options with zero arg *)
@@ -640,7 +639,7 @@ let init_toplevel arglist =
       engage ();
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
-      Syntax_def.set_compat_notations (not !no_compat_ntn);
+(*       Syntax_def.set_compat_notations (not !no_compat_ntn); FIXME *)
       if (not !batch_mode || List.is_empty !compile_list)
          && Global.env_is_initial ()
       then Option.iter Declaremods.start_library !toplevel_name;
@@ -677,7 +676,6 @@ 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
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index a48bbf89d..bbee39c3d 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -150,7 +150,7 @@ let alarm what internal msg =
   | UserAutomaticRequest
   | InternalTacticRequest ->
     (if debug then
-      Feedback.msg_warning
+      Feedback.msg_debug
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
   | _ -> Some msg
 
@@ -295,6 +295,11 @@ let declare_rewriting_schemes ind =
       (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind
   end
 
+let warn_cannot_build_congruence =
+  CWarnings.create ~name:"cannot-build-congruence" ~category:"schemes"
+         (fun () ->
+          strbrk "Cannot build congruence scheme because eq is not found")
+
 let declare_congr_scheme ind =
   if Hipattern.is_equality_type (mkInd ind) then begin
     if
@@ -303,7 +308,7 @@ let declare_congr_scheme ind =
     then
       ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
     else
-      Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
+      warn_cannot_build_congruence ()
   end
 
 let declare_sym_scheme ind =
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index c4c891b89..62aa85160 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -26,6 +26,11 @@ let check_locality locality_flag =
 
 (* Commands which supported an inlined Local flag *)
 
+let warn_deprecated_local_syntax =
+  CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated"
+         (fun () ->
+          Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.")
+
 let enforce_locality_full locality_flag local =
   let local =
     match locality_flag with
@@ -35,8 +40,8 @@ let enforce_locality_full locality_flag local =
 	Errors.error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
-          Feedback.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
-	  Some true
+	    warn_deprecated_local_syntax ();
+	    Some true
 	end else
 	None
     | Some b -> Some b in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e772ea020..aa6601a7d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -864,16 +864,23 @@ let check_rule_productivity l =
   if (match l with SProdList _ :: _ -> true | _ -> false) then
     error "A recursive notation must start with at least one symbol."
 
+let warn_notation_bound_to_variable =
+  CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing"
+         (fun () ->
+          strbrk "This notation will not be used for printing as it is bound to a single variable.")
+
+let warn_non_reversible_notation =
+  CWarnings.create ~name:"non-reversible-notation" ~category:"parsing"
+         (fun () ->
+          strbrk "This notation will not be used for printing as it is not reversible.")
+
 let is_not_printable onlyparse noninjective = function
 | NVar _ ->
-  let () = if not onlyparse then
-    Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
-  in
+  if not onlyparse then warn_notation_bound_to_variable ();
   true
 | _ ->
-  if not onlyparse && noninjective then
-    let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
-    true
+   if not onlyparse && noninjective then
+     (warn_non_reversible_notation (); true)
   else onlyparse
 
 let find_precedence lev etyps symbols =
@@ -928,6 +935,10 @@ let check_curly_brackets_notation_exists () =
     error "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved."
 
+let warn_skip_spaces_curly =
+  CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing"
+      (fun () ->strbrk "Skipping spaces inside curly brackets")
+
 (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
 let remove_curly_brackets l =
   let rec skip_break acc = function
@@ -942,9 +953,10 @@ let remove_curly_brackets l =
             let br',next' = skip_break [] l' in
             (match next' with
               | Terminal "}" as t2 :: l'' as l1 ->
-                  if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
-                    Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets");
-                  if deb && List.is_empty l'' then [t1;x;t2] else begin
+                 if not (List.equal Notation.symbol_eq l l0) ||
+		      not (List.equal Notation.symbol_eq l' l1) then
+		  warn_skip_spaces_curly ();
+		  if deb && List.is_empty l'' then [t1;x;t2] else begin
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
                   end
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 36c16208c..acd8026f9 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -146,7 +146,12 @@ let dir_ml_load s =
 let dir_ml_use s =
   match !load with
     | WithTop t -> t.use_file s
-    | _ -> Feedback.msg_warning (str "Cannot access the ML compiler")
+    | _ ->
+       let moreinfo =
+	 if Dynlink.is_native then " Loading ML code works only in bytecode."
+	 else ""
+       in
+      errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
 
 (* Adds a path to the ML paths *)
 let add_ml_dir s =
@@ -161,12 +166,22 @@ let add_rec_ml_dir unix_path =
 
 (* Adding files to Coq and ML loadpath *)
 
+let warn_cannot_use_directory =
+  CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem"
+         (fun d ->
+          str "Directory " ++ str d ++
+            strbrk " cannot be used as a Coq identifier (skipped)")
+
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
-    Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
+    warn_cannot_use_directory d;
     raise Exit
 
+let warn_cannot_open_path =
+  CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
+      (fun unix_path -> str "Cannot open " ++ str unix_path)
+
 let add_rec_path ~unix_path ~coq_root ~implicit =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
@@ -184,7 +199,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let () = List.iter add dirs in
     Loadpath.add_load_path unix_path ~implicit coq_root
   else
-    Feedback.msg_warning (str "Cannot open " ++ str unix_path)
+    warn_cannot_open_path unix_path
 
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index fe6ed55a7..3151b1372 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -173,6 +173,13 @@ type record_error =
   | MissingProj of Id.t * Id.t list
   | BadTypedProj of Id.t * env * Type_errors.type_error
 
+let warn_cannot_define_projection =
+  CWarnings.create ~name:"cannot-define-projection" ~category:"records"
+         (fun msg -> hov 0 msg)
+
+(* If a projection is not definable, we throw an error if the user
+asked it to be a coercion. Otherwise, we just print an info
+message. The user might still want to name the field of the record. *)
 let warning_or_error coe indsp err =
   let st = match err with
     | MissingProj (fi,projs) ->
@@ -197,7 +204,7 @@ let warning_or_error coe indsp err =
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then errorlabstrm "structure" st;
-  Flags.if_verbose Feedback.msg_warning (hov 0 st)
+  Flags.if_verbose Feedback.msg_info (hov 0 st)
 
 type field_status =
   | NoProjection of Name.t
@@ -240,6 +247,12 @@ let instantiate_possibly_recursive_type indu paramdecls fields =
   let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
   Termops.substl_rel_context (subst@[mkIndU indu]) fields
 
+let warn_non_primitive_record =
+  CWarnings.create ~name:"non-primitive-record" ~category:"record"
+         (fun (env,indsp) ->
+          (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ 
+                    strbrk" could not be defined as a primitive record")))
+
 (* We build projections *)
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
@@ -263,9 +276,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	| Some None | None -> false
       in
 	if not is_primitive then 
-	  Flags.if_verbose Feedback.msg_warning
-	    (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ 
-		      str" could not be defined as a primitive record"));
+	  warn_non_primitive_record (env,indsp);
 	is_primitive
     else false
   in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ac9293d5f..972d83055 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -18,14 +18,15 @@ open Vernacexpr
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-(* The navigation vernac commands will be handled separately *)
+(* Navigation commands are allowed in a coqtop session but not in a .v file *)
 
 let rec is_navigation_vernac = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
-  | VernacBack _ -> true
+  | VernacBack _
+  | VernacStm _ -> true
   | VernacRedirect (_, (_,c))
   | VernacTime (_,c) ->
       is_navigation_vernac c (* Time Back* is harmless *)
@@ -230,6 +231,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
+      CWarnings.set_current_loc (fst loc_ast);
       vernac_com verbosely checknav loc_ast
     done
   with any ->   (* whatever the exception *)
@@ -272,11 +274,17 @@ let load_vernac verb file =
     if !Flags.beautify_file then close_out !chan_beautify;
     iraise (disable_drop e, info)
 
+let warn_file_no_extension =
+  CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
+         (fun (f,ext) ->
+          str "File \"" ++ str f ++
+            strbrk "\" has been implicitly expanded to \"" ++
+            str f ++ str ext ++ str "\"")
+
 let ensure_ext ext f =
   if Filename.check_suffix f ext then f
   else begin
-    Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
-    expanded to \"" ++ str f ++ str ext ++ str "\"");
+    warn_file_no_extension (f,ext);
     f ^ ext
   end
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 82fe9751e..65aa46bc1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -896,7 +896,11 @@ let vernac_chdir = function
   | Some path ->
       begin
 	try Sys.chdir (expand path)
-	with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err)
+	with Sys_error err ->
+	  (* Cd is typically used to control the output directory of
+	  extraction. A failed Cd could lead to overwriting .ml files
+	  so we make it an error. *)
+	  Errors.error ("Cd failed: " ^ err)
       end;
       if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
@@ -943,6 +947,16 @@ let vernac_declare_implicits locality r l =
       Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
+let warn_arguments_assert =
+  CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
+         (fun sr ->
+          strbrk "This command is just asserting the number and names of arguments of " ++
+            pr_global sr ++ strbrk". If this is what you want add " ++
+            strbrk "': assert' to silence the warning. If you want " ++
+            strbrk "to clear implicit arguments add ': clear implicits'. " ++
+            strbrk "If you want to clear notation scopes add ': clear scopes'")
+         
+
 let vernac_declare_arguments locality r l nargs flags =
   let extra_scope_flag = List.mem `ExtraScopes flags in
   let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
@@ -1071,7 +1085,7 @@ let vernac_declare_arguments locality r l nargs flags =
           some_scopes_specified ||
           some_simpl_flags_specified) &&
      no_flags then
-    Feedback.msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
+    warn_arguments_assert sr
 
 
 let default_env () = {
@@ -1342,6 +1356,15 @@ let _ =
       optread  = (fun () -> !Constrintern.parsing_explicit);
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
 
+let _ =
+  declare_string_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "warnings display";
+      optkey   = ["Warnings"];
+      optread  = CWarnings.get_flags;
+      optwrite = CWarnings.set_flags }
+
 let vernac_set_strategy locality l =
   let local = make_locality locality in
   let glob_ref r =
@@ -1855,12 +1878,12 @@ let interp ?proof ~loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbort id -> Feedback.msg_warning (str "VernacAbort not handled by Stm")
-  | VernacAbortAll -> Feedback.msg_warning (str "VernacAbortAll not handled by Stm")
-  | VernacRestart -> Feedback.msg_warning (str "VernacRestart not handled by Stm")
-  | VernacUndo _ -> Feedback.msg_warning (str "VernacUndo not handled by Stm")
-  | VernacUndoTo _ -> Feedback.msg_warning (str "VernacUndoTo not handled by Stm")
-  | VernacBacktrack _ -> Feedback.msg_warning (str "VernacBacktrack not handled by Stm")
+  | VernacAbort id -> Errors.errorlabstrm "" (str "Abort cannot be used through the Load command")
+  | VernacAbortAll -> Errors.errorlabstrm "" (str "AbortAll cannot be used through the Load command")
+  | VernacRestart -> Errors.errorlabstrm "" (str "Restart cannot be used through the Load command")
+  | VernacUndo _ -> Errors.errorlabstrm "" (str "Undo cannot be used through the Load command")
+  | VernacUndoTo _ -> Errors.errorlabstrm "" (str "UndoTo cannot be used through the Load command")
+  | VernacBacktrack _ -> Errors.errorlabstrm "" (str "Backtrack cannot be used through the Load command")
   
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 1116a3104..0abc9e76d 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -42,6 +42,11 @@ let vinterp_map s =
 
 let vinterp_init () = Hashtbl.clear vernac_tab
 
+let warn_deprecated_command =
+  let open CWarnings in
+  create ~name:"deprecated-command" ~category:"deprecated"
+         (fun pr -> str "Deprecated vernacular command: " ++ pr)
+
 (* Interpretation of a vernac command *)
 
 let call ?locality (opn,converted_args) =
@@ -55,7 +60,7 @@ let call ?locality (opn,converted_args) =
       | Egramml.GramNonTerminal _ -> str "_"
       in
       let pr = pr_sequence pr_gram rules in
-      Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr)
+      warn_deprecated_command pr;
     in
     loc:= "Checking arguments";
     let hunk = callback converted_args in