summaryrefslogtreecommitdiff
path: root/interp/reserve.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /interp/reserve.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'interp/reserve.ml')
-rw-r--r--interp/reserve.ml20
1 files changed, 10 insertions, 10 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 3ec0182b..f7496832 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 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: reserve.ml 10727 2008-03-28 20:22:43Z msozeau $ i*)
(* Reserved names *)
@@ -54,22 +54,22 @@ open Rawterm
let rec unloc = function
| RVar (_,id) -> RVar (dummy_loc,id)
| RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
- | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c)
- | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c)
+ | 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)
- | RCases (_,rtntypopt,tml,pl) ->
- RCases (dummy_loc,
- (option_map unloc rtntypopt),
+ | RCases (_,sty,rtntypopt,tml,pl) ->
+ RCases (dummy_loc,sty,
+ (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_map 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_map 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_map unloc obd, unloc ty)))
+ (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
bl,
Array.map unloc tyl,
Array.map unloc bv)
@@ -85,7 +85,7 @@ let rec unloc = function
let anonymize_if_reserved na t = match na with
| Name id as na ->
(try
- if unloc t = find_reserved_type id
+ if not !Flags.raw_print & unloc t = find_reserved_type id
then RHole (dummy_loc,Evd.BinderType na)
else t
with Not_found -> t)