From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 interp/reserve.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'interp/reserve.ml')

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)
-- 
cgit v1.2.3