package rocq-runtime

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

Parameter MakeWarned.M

Common APIs on name tables.

type elt

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

val push : visibility -> Libnames.full_path -> elt -> unit

Add an element or modify its visibility. With visibility Until, assume the element is new. With visibility Exactly, assume the element is not new.

val 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 : Libnames.qualid -> elt

Globalize the given user-level reference. If any warnings are associated with the produced object, print them unless nowarn:true was given.

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.