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, 2 insertions, 1 deletions
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)