Module Term_dnetSource

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.