diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 917f9f4ad..834587f8d 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -57,14 +57,11 @@ let rec unloc = function | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c) | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RCases (_,(tyopt,rtntypopt),tml,pl) -> + | RCases (_,rtntypopt,tml,pl) -> RCases (dummy_loc, - (option_app unloc tyopt,ref (option_app unloc !rtntypopt)), + (option_app unloc rtntypopt), List.map (fun (tm,x) -> (unloc tm,x)) tml, List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) - | 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) | RIf (_,c,(na,po),b1,b2) -> @@ -86,7 +83,6 @@ let rec unloc = function let anonymize_if_reserved na t = match na with | Name id as na -> - if !Options.v7 & id = id_of_string "_" then t else (try if unloc t = find_reserved_type id then RHole (dummy_loc,Evd.BinderType na) |