diff options
| author | glondu | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /interp/reserve.ml | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 93fc60dfb2..9d8412825f 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -24,22 +24,22 @@ let cache_reserved_type (_,(id,t)) = reserve_table := Idmap.add id t !reserve_table let (in_reserved, _) = - declare_object {(default_object "RESERVED-TYPE") with + declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } -let _ = +let _ = Summary.declare_summary "reserved-type" { Summary.freeze_function = (fun () -> !reserve_table); Summary.unfreeze_function = (fun r -> reserve_table := r); Summary.init_function = (fun () -> reserve_table := Idmap.empty) } -let declare_reserved_type (loc,id) t = +let declare_reserved_type (loc,id) t = if id <> root_of_id id then user_err_loc(loc,"declare_reserved_type", (pr_id id ++ str " is not reservable: it must have no trailing digits, quote, or _")); begin try - let _ = Idmap.find id !reserve_table in + let _ = Idmap.find id !reserve_table in user_err_loc(loc,"declare_reserved_type", (pr_id id++str" is already bound to a type")) with Not_found -> () end; @@ -66,7 +66,7 @@ let rec unloc = function 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 + Array.map (List.map (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty))) bl, Array.map unloc tyl, @@ -82,7 +82,7 @@ let rec unloc = function let anonymize_if_reserved na t = match na with | Name id as na -> - (try + (try if not !Flags.raw_print & unloc t = find_reserved_type id then RHole (dummy_loc,Evd.BinderType na) else t |