package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

doc/coq-core.lib/Loc/index.html

Module LocSource

Basic types
Sourcetype source =
  1. | InFile of {
    1. dirpath : string option;
    2. file : string;
    }
  2. | ToplevelInput
Sourcetype t = {
  1. fname : source;
    (*

    filename or toplevel input

    *)
  2. line_nb : int;
    (*

    start line number

    *)
  3. bol_pos : int;
    (*

    position of the beginning of start line

    *)
  4. line_nb_last : int;
    (*

    end line number

    *)
  5. bol_pos_last : int;
    (*

    position of the beginning of end line

    *)
  6. bp : int;
    (*

    start position

    *)
  7. ep : int;
    (*

    end position

    *)
}
Location manipulation

This is inherited from CAMPL4/5.

Sourceval create : source -> int -> int -> int -> int -> t

Create a location from a filename, a line number, a position of the beginning of the line, a start and end position

Sourceval initial : source -> t

Create a location corresponding to the beginning of the given source

Sourceval unloc : t -> int * int

Return the start and end position of a location

Sourceval make_loc : (int * int) -> t

Make a location out of its start and end position

Sourceval merge : t -> t -> t
Sourceval merge_opt : t option -> t option -> t option

Merge locations, usually generating the largest possible span

Sourceval sub : t -> int -> int -> t

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.

Sourceval after : t -> int -> int -> t

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.

Sourceval finer : t option -> t option -> bool

Answers true when the first location is more defined, or, when both defined, included in the second one

Sourceval shift_loc : int -> int -> t -> t

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
Sourceval add_loc : Exninfo.info -> t -> Exninfo.info

Adding location to an exception

Sourceval get_loc : Exninfo.info -> t option

Retrieving the optional location of an exception

Sourceval raise : ?loc:t -> exn -> 'a

raise loc e is the same as Pervasives.raise (add_loc e loc).

Objects with location information
Sourcetype 'a located = t option * 'a
Sourceval tag : ?loc:t -> 'a -> 'a located

Embed a location in a type

Sourceval map : ('a -> 'b) -> 'a located -> 'b located

Modify an object carrying a location

Sourceval pr : t -> Pp.t

Print for user consumption.