Index of types


E
envs [Theory.Trans]
ext_units [Matcher]

G
goal_sigma [Coq]

H
hypinfo [Coq.Rewrite]
We keep some informations about the hypothesis, with an (informal) invariant: typeof hyp = typ, typ = forall context, body, body = rel left right

I
ir [Theory.Trans]

M
m [Search_monad]
A data type that represent a collection of 'a
mset [Matcher]
The arguments of sums (or AC operators) are represented using finite multisets.

N
nf_term [Matcher.Terms]

P
pack [Theory.Sym]
mimics the Coq record Sym.pack

R
reifier [Theory.Trans]
We need to reify two terms (left and right members of a goal) that share the same reification envirnoment.

S
sigmas [Theory.Trans]
symbol [Matcher]

T
t [Matcher.Subst]
t [Matcher.Terms]
t [Coq.Equivalence]
t [Coq.Transitive]
t [Coq.Relation]

U
units [Matcher]

V
var [Matcher]