Make (coq-core.Nametab.Make)

Parameters

module U : UserName

module E : EqualityType

type elt = E.t

type t

type user_name = U.t

val empty : t

val push : visibility -> user_name -> elt -> t -> t

val locate : Libnames.qualid -> t -> elt

val find : user_name -> t -> elt

val remove : user_name -> t -> t

val exists : user_name -> t -> bool

val user_name : Libnames.qualid -> t -> user_name

val shortest_qualid_gen : 
  ?loc:Loc.t ->
  ( Names.Id.t -> bool ) ->
  user_name ->
  t ->
  Libnames.qualid

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

val find_prefixes : Libnames.qualid -> t -> elt list

val match_prefixes : Libnames.qualid -> t -> elt list