aboutsummaryrefslogtreecommitdiff
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 d6305d81a8..3344faef8a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -348,8 +348,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");
- pat_of_raw metas vars c
+ Errors.error ("Cast not supported in constr pattern")
| GIf (_,c,(_,None),b1,b2) ->
PIf (pat_of_raw metas vars c,
pat_of_raw metas vars b1,pat_of_raw metas vars b2)