Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.

2 files changed, 19 insertions, 22 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 50dceb8e6b..a2e8fac059 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -301,16 +301,13 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident =
 
 (* Admitted *)
 
-let warn_let_as_axiom =
-  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
-                                spc () ++ strbrk "declared as an axiom.")
-
 let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
+  | Local, _, _ | Discharge, _, _ ->
+    Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+      str "declared as an axiom.")
   in
   let () = assumption_message id in
   Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
diff --git a/stm/stm.ml b/stm/stm.ml
index 3fb3a2f321..d460cea943 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -989,6 +989,8 @@ end = struct (* {{{ *)
       | VernacResetInitial ->
           VtStm (VtBack Stateid.initial, true), VtNow
       | VernacResetName (_,name) ->
+          msg_warning
+            (str"Reset not implemented for automatically generated constants");
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
             let oid =
@@ -1038,8 +1040,8 @@ end = struct (* {{{ *)
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
-       Errors.errorlabstrm "undo_vernac_classifier"
-        (str "Cannot undo")
+       msg_warning(str"undo_vernac_classifier: going back to the initial state.");
+       VtStm (VtBack Stateid.initial, true), VtNow
 
 end (* }}} *)
 
@@ -1366,7 +1368,7 @@ end = struct (* {{{ *)
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_debug (str "STM: sending back a fat state");
+          msg_warning (str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
@@ -1896,12 +1898,6 @@ let delegate name =
   || !Flags.compilation_mode = Flags.BuildVio
   || !Flags.async_proofs_full
  
-let warn_deprecated_nested_proofs =
-  CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
-         (fun () ->
-          strbrk ("Nested proofs are deprecated and will "^
-                    "stop working in a future Coq version"))
-
 let collect_proof keep cur hd brkind id =
  prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
@@ -1966,7 +1962,8 @@ let collect_proof keep cur hd brkind id =
         let name = name ids in
         `MaybeASync (parent last, None, accn, name, delegate name)
     | `Sideff _ ->
-       warn_deprecated_nested_proofs ();
+        Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^
+           "stop working in the next Coq version")));
         `Sync (no_name,None,`NestedProof)
     | _ -> `Sync (no_name,None,`Unknown) in
  let make_sync why = function
@@ -2413,7 +2410,10 @@ let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty
-  ({ verbose; loc; expr } as x) c =
+  ({ verbose; loc; expr } as x) c
+ =
+  let warn_if_pos a b =
+    if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
   prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
   let vcs = VCS.backup () in
   try
@@ -2427,12 +2427,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
       | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
       (* Joining various parts of the document *)
-      | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
-      | VtStm (VtFinish, b),       VtNow -> finish (); `Ok
-      | VtStm (VtWait, b),     VtNow -> finish (); wait (); `Ok
+      | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok
+      | VtStm (VtFinish, b),       VtNow -> warn_if_pos x b; finish (); `Ok
+      | VtStm (VtWait, b),     VtNow -> warn_if_pos x b; finish (); wait (); `Ok
       | VtStm (VtPrintDag, b), VtNow ->
-          VCS.print ~now:true (); `Ok
-      | VtStm (VtObserve id, b),   VtNow -> observe id; `Ok
+          warn_if_pos x b; VCS.print ~now:true (); `Ok
+      | VtStm (VtObserve id, b),   VtNow -> warn_if_pos x b; observe id; `Ok
       | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
                 |VtPrintDag |VtWait),_), VtLater ->
           anomaly(str"classifier: join actions cannot be classified as VtLater")