From 8e07227c5853de78eaed4577eefe908fb84507c0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 28 Jun 2016 10:55:30 +0200
Subject: 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
---
 pretyping/patternops.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d6305d81a8..7eb3d633da 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -317,6 +317,10 @@ let rev_it_mkPLambda = List.fold_right mkPLambda
 
 let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
 
+let warn_cast_in_pattern =
+  CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
+    (fun () -> Pp.strbrk "Casts are ignored in patterns")
+
 let rec pat_of_raw metas vars = function
   | GVar (_,id) ->
       (try PRel (List.index Name.equal (Name id) vars)
@@ -348,7 +352,7 @@ let rec pat_of_raw metas vars = function
   | GHole _ ->
       PMeta None
   | GCast (_,c,_) ->
-      Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern");
+      warn_cast_in_pattern ();
       pat_of_raw metas vars c
   | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
-- 
cgit v1.2.3