package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/coq-core.lib/Loc/index.html
Module Loc
Source
Basic types
type t = {
fname : source;
(*filename or toplevel input
*)line_nb : int;
(*start line number
*)bol_pos : int;
(*position of the beginning of start line
*)line_nb_last : int;
(*end line number
*)bol_pos_last : int;
(*position of the beginning of end line
*)bp : int;
(*start position
*)ep : int;
(*end position
*)
}
Location manipulation
This is inherited from CAMPL4/5.
Create a location from a filename, a line number, a position of the beginning of the line, a start and end position
Merge locations, usually generating the largest possible span
sub loc sh len
is the location loc
shifted with sh
characters and with length len
. The previous ending position of the location is lost.
after loc sh len
is the location just after loc (starting at the end position of loc
) shifted with sh
characters and of length len
.
Answers true
when the first location is more defined, or, when both defined, included in the second one
shift_loc loc n p
shifts the beginning of location by n
and the end by p
; it is assumed that the shifts do not change the lines at which the location starts and ends
Located exceptions
Adding location to an exception
Retrieving the optional location of an exception