aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--interp/reserve.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 5287ce5a2d..daffc3945a 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -51,6 +51,8 @@ let rec unloc = function
| ROrderedCase (_,b,tyopt,tm,bv,x) ->
ROrderedCase
(dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x)
+ | RLetTuple (_,nal,(na,po),b,c) ->
+ RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
| RRec (_,fk,idl,tyl,bv) ->
RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv)
| RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)