X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAst.ml;h=ca48567863aa8d9c88ebf6eba9aa986db55c1fae;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=9abd07a75836d6c38ff53e65672fce017d1e5544;hpb=714376413f68dad720d6253b1f36209d8d096443;p=helm.git diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml index 9abd07a75..ca4856786 100644 --- a/helm/ocaml/cic_transformations/cicAst.ml +++ b/helm/ocaml/cic_transformations/cicAst.ml @@ -28,11 +28,13 @@ open Printf type location = Lexing.position * Lexing.position let pp_location (loc_begin, loc_end) = - sprintf "(%d,%d)-(%d,%d)" - loc_begin.Lexing.pos_lnum - (loc_begin.Lexing.pos_cnum - loc_begin.Lexing.pos_bol) - loc_end.Lexing.pos_lnum - (loc_end.Lexing.pos_cnum - loc_end.Lexing.pos_bol) + let c_begin = loc_begin.Lexing.pos_cnum - loc_begin.Lexing.pos_bol in + let c_end = loc_end.Lexing.pos_cnum - loc_end.Lexing.pos_bol in + if loc_begin.Lexing.pos_lnum = -1 || loc_end.Lexing.pos_lnum = -1 then + sprintf "%d-%d" c_begin c_end + else + sprintf "(%d,%d)-(%d,%d)" loc_begin.Lexing.pos_lnum c_begin + loc_end.Lexing.pos_lnum c_end let floc_of_loc (loc_begin, loc_end) = let floc_begin =