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.

8 files changed, 28 insertions, 41 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index d3d4201f57..55220f44c0 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
   if is_ambig && is_verbose () then
-    Feedback.msg_info (message_ambig !ambig_paths)
+    Feedback.msg_warning (message_ambig !ambig_paths)
 
 type coercion = {
   coercion_type   : coe_typ;
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index c566839e85..129725c6d2 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -49,12 +49,12 @@ type bound_ident_map = Id.t Id.Map.t
 
 exception PatternMatchingFailure
 
-let warn_meta_collision =
-  CWarnings.create ~name:"meta-collision" ~category:"ltac"
-         (fun name ->
-          strbrk "Collision between bound variable " ++ pr_id name ++
-            strbrk " and a metavariable of same name.")
+let warn_bound_meta name =
+  Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++
+    str " and a metavariable of same name.")
 
+let warn_bound_bound name =
+  Feedback.msg_warning (str "Collision between bound variables of name " ++ pr_id name)
 
 let constrain n (ids, m as x) (names, terms as subst) =
   try
@@ -62,19 +62,18 @@ let constrain n (ids, m as x) (names, terms as subst) =
     if List.equal Id.equal ids ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with Not_found ->
-    let () = if Id.Map.mem n names then warn_meta_collision n in
+    let () = if Id.Map.mem n names then warn_bound_meta n in
     (names, Id.Map.add n x terms)
 
 let add_binders na1 na2 binding_vars (names, terms as subst) =
   match na1, na2 with
   | Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
     if Id.Map.mem id1 names then
-      let () = Glob_ops.warn_variable_collision id1 in
+      let () = warn_bound_bound id1 in
       (names, terms)
     else
       let names = Id.Map.add id1 id2 names in
-      let () = if Id.Map.mem id1 terms then
-        warn_meta_collision id1 in
+      let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in
       (names, terms)
   | _ -> subst
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cc178eb975..86921c49b0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t =
         share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
-        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+        if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
         let c = detype flags avoid env sigma c in
         let t = detype flags avoid env sigma t in
         (List.rev l,c,t)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5c8060996a..04100c8a73 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -334,14 +334,10 @@ let glob_visible_short_qualid c =
         fold_glob_constr aux acc c
   in aux [] c
 
-let warn_variable_collision =
-  let open Pp in
-  CWarnings.create ~name:"variable-collision" ~category:"ltac"
-         (fun name ->
-          strbrk "Collision between bound variables of name " ++ pr_id name)
-
 let add_and_check_ident id set =
-  if Id.Set.mem id set then warn_variable_collision id;
+  if Id.Set.mem id set then
+    Feedback.msg_warning
+      Pp.(str "Collision between bound variables of name " ++ Id.print id);
   Id.Set.add id set
 
 let bound_glob_vars =
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c2b27ca6ab..e0a2de0326 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -34,8 +34,6 @@ val map_glob_constr :
 val map_glob_constr_left_to_right :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
 
-val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
-
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index fc38e98c63..5d36fc78ef 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -183,7 +183,9 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
               | ra::rest ->
                   (match dest_recarg ra with
 	            | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
-	            | Imbr _  -> (None,rest)
+	            | Imbr _  ->
+		        Feedback.msg_warning (strbrk "Ignoring recursive call");
+		        (None,rest)
                     | _ -> (None, rest))
 	  in
           (match optionpos with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3344faef8a..d6305d81a8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -348,7 +348,8 @@ let rec pat_of_raw metas vars = function
   | GHole _ ->
       PMeta None
   | GCast (_,c,_) ->
-      Errors.error ("Cast not supported in constr pattern")
+      Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern");
+      pat_of_raw metas vars c
   | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 2959bd7c84..bbb6a92663 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -187,13 +187,6 @@ let cs_pattern_of_constr t =
           with e when Errors.noncritical e -> raise Not_found
 	end
 
-let warn_projection_no_head_constant =
-  CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
-         (fun (t,con_pp,proji_sp_pp) ->
-          strbrk "Projection value has no head constant: "
-          ++ Termops.print_constr t ++ strbrk " in canonical instance "  
-          ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
-
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let env = Global.env () in
@@ -220,10 +213,13 @@ let compute_canonical_projections (con,ind) =
 		   let patt, n , args = cs_pattern_of_constr t in
 		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
-                     let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
+                   if Flags.is_verbose () then
+                     (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-                     warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
-                   l
+		      Feedback.msg_warning (strbrk "No global reference exists for projection value"
+                                   ++ Termops.print_constr t ++ strbrk " in instance "  
+                                   ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it."));
+		   l
 	       end
 	   | _ -> l)
       [] lps in
@@ -239,13 +235,6 @@ let pr_cs_pattern = function
   | Default_cs -> str "_"
   | Sort_cs s -> Termops.pr_sort_family s
 
-let warn_redundant_canonical_projection =
-  CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
-         (fun (hd_val,prj,new_can_s,old_can_s) ->
-          strbrk "Ignoring canonical projection to " ++ hd_val
-          ++ strbrk " by " ++ prj ++ strbrk " in "
-          ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
-
 let open_canonical_structure i (_,o) =
   if Int.equal i 1 then
     let lo = compute_canonical_projections o in
@@ -256,12 +245,14 @@ let open_canonical_structure i (_,o) =
       in match ocs with
         | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
+            if Flags.is_verbose () then
               let old_can_s = (Termops.print_constr cs.o_DEF)
               and new_can_s = (Termops.print_constr s.o_DEF) in
               let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
-              warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
-          lo
+              Feedback.msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
+                             ++ strbrk " by " ++ prj ++ strbrk " in "
+                             ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo
 
 let cache_canonical_structure o =
   open_canonical_structure 1 o