package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.library/Nametab/Easy/index.html

Module Nametab.EasySource

Generate a nametab with simple warning support (UserWarn.create_depr_and_user_warnings_qf).

NAMETAB extended with warnings associated to some of the elements.

Parameters

module M : sig ... end

Signature

include NAMETAB with type elt = M.t
Sourcetype elt = M.t

The type of the elements of the name table (eg ModPath.t)

Sourceval remove : Libnames.full_path -> elt -> unit

Remove an element.

Sourceval shortest_qualid_gen : ?loc:Loc.t -> ?force_short:bool -> (Names.Id.t -> bool) -> elt -> Libnames.qualid

shortest_qualid_gen avoid v: given an object v with full name Mylib.A.B.x, try to find the shortest among x, B.x, A.B.x and Mylib.A.B.x that denotes the same object. If avoid is true on x it is assumed to denote something else (so B.x is the shortest qualid that could be returned). If ~force_short:true is passed, always returns the shortest qualid. Otherwise, respects the "Printing Fully Qualified" flag.

Sourceval shortest_qualid : ?loc:Loc.t -> ?force_short:bool -> Names.Id.Set.t -> elt -> Libnames.qualid

Like shortest_qualid_gen but using an id set instead of a closure.

Sourceval pr : elt -> Pp.t

Print using shortest_qualid and empty avoid set.

Sourceval locate_upto : limit:int -> Libnames.qualid -> (Libnames.qualid * elt) list

Find elements which are limit different from the input (dots are treated rigidly).

Sourceval locate_all : Libnames.qualid -> elt list

Locate all elements with a given suffix. If the qualid is a valid absolute name, that element is first in the list.

Sourceval completion_candidates : Libnames.qualid -> elt list

Return the elements that have the qualid as a prefix. UIs will usually compose with shortest_qualid. Experimental APIs, please tell us if you use it.

Sourceval to_path : elt -> Libnames.full_path

Return the absolute name for the given element.

Sourceval of_path : Libnames.full_path -> elt

Return an element bound to an absolute path.

Sourceval exists : Libnames.full_path -> bool

Returns whether this absolute path is taken.

Sourceval push : ?wdata:M.t UserWarn.with_qf -> visibility -> Libnames.full_path -> elt -> unit

When visibility is Until, wdata may be Some _ in which case the warning data is associated to the element.

Sourceval is_warned : elt -> M.t UserWarn.with_qf option

Return the warning data associated to the element.

Sourceval warn : ?loc:Loc.t -> elt -> M.t UserWarn.with_qf -> unit

Emit the given warning data for the given element (if the warning is not disabled).

Sourceval locate : ?nowarn:bool -> Libnames.qualid -> elt

Unless nowarn:false is given, if the found element is associated to a warning, that warning is emitted.