package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 (Ident : IDENT) (Opt : OPT) : S with type ident = Ident.t