summaryrefslogtreecommitdiff
path: root/interp/reserve.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /interp/reserve.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'interp/reserve.ml')
-rw-r--r--interp/reserve.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 476fd7e6..aee981bd 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.ml 7732 2005-12-26 13:51:24Z herbelin $ i*)
+(*i $Id: reserve.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
(* Reserved names *)
@@ -59,17 +59,17 @@ let rec unloc = function
| RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
| RCases (_,rtntypopt,tml,pl) ->
RCases (dummy_loc,
- (option_app unloc rtntypopt),
+ (option_map unloc rtntypopt),
List.map (fun (tm,x) -> (unloc tm,x)) tml,
List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
| RLetTuple (_,nal,(na,po),b,c) ->
- RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
+ RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c)
| RIf (_,c,(na,po),b1,b2) ->
- RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
+ RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2)
| RRec (_,fk,idl,bl,tyl,bv) ->
RRec (dummy_loc,fk,idl,
Array.map (List.map
- (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty)))
+ (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty)))
bl,
Array.map unloc tyl,
Array.map unloc bv)