Module type `Goptions.TableArg`

The functor MakeTable declares a table. Vernacular Add, Remove, and Test commands pass each argument as a table_value; encode maps such values to stored elements, possibly globalizing qualified identifiers with the supplied environment. Tables that do not support one of the constructors should raise a user error from encode.

type t

module Set : ArgSet with type elt = t

val encode : Environ.env -> table_value -> t

val subst : Mod_subst.substitution -> t -> t

val check_local : Libobject.locality -> t -> unit

val discharge : t -> t

Elements which cannot be discharged should only be added with Local

val printer : t -> Pp.t

val key : option_name

val title : string

val member_message : t -> bool -> Pp.t