aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/whelp.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index d76c281be..8396987ff 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -164,7 +164,7 @@ let rec uri_of_constr c =
uri_of_constr b; url_string " in "; uri_of_constr c
| RCast (_,c, CastConv (_,t)) ->
uri_of_constr c; url_string ":"; uri_of_constr t
- | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+ | RRec _ | RIf _ | RLetTuple _ | RLetPattern _ | RCases _ ->
error "Whelp does not support pattern-matching and (co-)fixpoint"
| RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
anomaly "Written w/o parenthesis"