aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/whelp.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/whelp.ml4')
-rw-r--r--toplevel/whelp.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 094c93196..82a2a8449 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -166,8 +166,8 @@ 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
- | RRecord _ | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
- error "Whelp does not support records, pattern-matching and (co-)fixpoint."
+ | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+ error "Whelp does not support pattern-matching and (co-)fixpoint."
| RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
anomaly "Written w/o parenthesis"
| RPatVar _ | RDynamic _ ->