Module `Term_dnet`

Dnets on constr terms.

An instantiation of Dnet on (an approximation of) constr. It associates a term (possibly with Evar) with an identifier. Identifiers must be unique (no two terms sharing the same ident), and there must be a way to recover the full term from the identifier (function constr_of).

Optionally, a pre-treatment on terms can be performed before adding or searching (reduce). Practically, it is used to do some kind of delta-reduction on terms before indexing them.

The results returned here are perfect, since post-filtering is done inside here.

See tactics/dnet.mli for more details.

module type IDENT = sig ... end: Identifiers to store (right hand side of the association)

module type OPT = sig ... end: Options :

module type S = sig ... end

module Make : functor (Ident : IDENT) -> functor (Opt : OPT) -> S with type ident = Ident.t