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] |