E | |
| envs [Theory.Trans] | |
| ext_units [Matcher] | |
H | |
| hypinfo [Coq.Rewrite] | We keep some informations about the hypothesis, with an (informal)
invariant: |
I | |
| ir [Theory.Trans] | |
L | |
| lazy_ref [Coq] | Getting Coq terms from the environment |
M | |
| m [Search_monad] | A data type that represent a collection of |
| 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 |
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.Relation] | |
| tactic [Coq] | |
U | |
| units [Matcher] | |
V | |
| var [Matcher] |