diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 2479f1f04..f49c42a55 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -57,7 +57,6 @@ let rec unloc = function | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RRecord (_,w,l) -> RRecord (dummy_loc,w,l) | RCases (_,sty,rtntypopt,tml,pl) -> RCases (dummy_loc,sty, (Option.map unloc rtntypopt), |