Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
(** This module centralizes the notions of hooks. Hooks are pointers that are to be set at runtime exactly once. *)
type 'a t(** The type of hooks containing ['a]. Hooks can only be set. *)
type 'a value(** The content part of a hook. *)
val make : unit -> ('a value * 'a t)(** Create a new hook together with a way to retrieve its runtime value. *)
val get : 'a value -> 'a(** Access the content of a hook. If it was not set yet, try to recover the default value if there is one. @raise Assert_failure if undefined. *)
val set : 'a t -> 'a -> unit(** Register a hook. Assertion failure if already registered. *)