package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Nametab.MakeWarnedSource

Add warning support to an existing nametab.

NAMETAB extended with warnings associated to some of the elements.

Parameters

module M : NAMETAB
module W : WarnInfo with type elt = M.elt

Signature

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

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

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

Remove an element.

val shortest_qualid_gen : ?loc:Loc.t -> (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).

val shortest_qualid : ?loc:Loc.t -> Names.Id.Set.t -> elt -> Libnames.qualid

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

val pr : elt -> Pp.t

Print using shortest_qualid and empty avoid set.

val 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.

val 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.

val to_path : elt -> Libnames.full_path

Return the absolute name for the given element.

val of_path : Libnames.full_path -> elt

Return an element bound to an absolute path.

val exists : Libnames.full_path -> bool

Returns whether this absolute path is taken.

Sourceval push : ?wdata:W.data -> 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 -> W.data option

Return the warning data associated to the element.

Sourceval warn : ?loc:Loc.t -> elt -> W.data -> 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.