summaryrefslogtreecommitdiff
path: root/parsing/ppconstr.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
commit4767d724d489a7ad67f696e9401e70b9f9ae2143 (patch)
tree142a99bc1cd3beef403f1942908de090f70c5e07 /parsing/ppconstr.ml
parent72b9a7df489ea47b3e5470741fd39f6100d31676 (diff)
Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r--parsing/ppconstr.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 275e179e..92c6715e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: ppconstr.ml 10087 2007-08-24 10:39:30Z herbelin $ *)
(*i*)
open Util
@@ -95,9 +95,9 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
let pr_delimiters key strm =
strm ++ str ("%"^key)
-let pr_located pr ((b,e),x) =
- if Options.do_translate() && (b,e)<>dummy_loc then
- let (b,e) = unloc (b,e) in
+let pr_located pr (loc,x) =
+ if Options.do_translate() && loc<>dummy_loc then
+ let (b,e) = unloc loc in
comment b ++ pr x ++ comment e
else pr x
@@ -142,7 +142,7 @@ let pr_opt_type_spc pr = function
| CHole _ -> mt ()
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
if loc <> dummy_loc then
let (b,_) = unloc loc in
pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)