aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/patternops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/patternops.ml')
-rw-r--r--pretyping/patternops.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d227e1f2a..5e4e5eb97 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -330,8 +330,7 @@ let rec pat_of_raw metas vars = function
| GHole _ ->
PMeta None
| GCast (_,c,_) ->
- Flags.if_warn
- Pp.msg_warning (strbrk "Cast not taken into account in constr pattern");
+ Pp.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,