Observer (p.rocq-runtime.9.2.0.doc.rocq-runtime.vernac.Vernacentries.DefAttributes.Observer)

Sourcetype token

The type of tokens to manipulate values. This is always marshallable.

Sourcetype value = unit Declare.Hook.g list Attributes.attribute

The value being stored. May be non-marshallable (typically a closure).

Sourceval register : name:string -> ?override:bool -> value -> token

Register a new value and get the token used to enable and disable it.

Sourceval activate : token -> unit

Activate/deactive the value attached to the token.

Sourceval deactivate : token -> unit

Sourceval is_active : token -> bool

Determine if the value for the given token is active.