package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2
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