Rewrote expressions to incorporate dependent types, now terms and types are mixed, still to rewrite the typing procedure.
Finished implementing the term structure and the abstraction and substitution functions.
Added structural term equality. Note that terms which are known to be proofs are not compared.
Basic type inference and obligation generation for the core language
added the trivial obligation solver
corrected bug in typing, added tag to constants indicating whether to check type or not
renamed the constr module to goals, slight rewrite of the trivial solver
correct constr -> goals
Added rich information to terms, and dark magic which allows terms to be parsed and pretty printed
according to information in the info class. Functions can be decorated to return an Expr with a given info
term as its information, by using infobox.
Corrected bugs in typing; info is now "sticky" in substitution and instanciation: the substituted term will have the same info tag as the original term. Corrected printing bug.
Added contexts, which are simply a dictionary of dictionaries tracking
current information.

Corrected a number of bugs regarding the interaction of info and typing/expression creation.
Added some facilities for defining terms and adding them to the context, and checking the type of terms in general. Also there is a "unsolved_goals" field in a context, and one can pop it to get the next unsolved goal.
Removed some syntactic idiosyncrasies.
Added beta conversion, functions can be 'parallel reduced' to compare forms in which -existing- beta-redexes are eliminated. Beta includes ordinary beta-reduction, projection of a tuple, and taking the contents out of a box. Added a method to solve goals by first performing reduction, then calling the trivial solver.
A class for fresh variable generation
Redesigned the tactic process: now tactics are a class, and return a list of subgoals.
Goals now depend on a context, so the context module has been moved into the core directory.
The trivial tactic checks the hypotheses to see if any can be directly applied.
The simpl tactic applies parrallel beta-reduction to the goal, and calls trivial on it.
added a destruct tactic that makes progress on goals of type A <= B (but does not solve them)
try and composition tactics added to goals
Sig now does not depend on a telescope but is handled uniformly as the other binders. The Expr objects do not inherit fields from the info dictionary anymore, so one has to type e.info.my_field instead of e.my_field. This makes understanding errors much easier, as the e.my_field returned None when the field was not present in the dictionary.

Elab creates the basic framework for implicit types. Types can be marked as implicit, and when a term is applied to others, the elaboration function fills blanks with fresh meta-variables. Note that this will require duplicating type names: nat and nat_implicit, with identical names (but different tags).

The unification constraints are not solved for now.
Corrected a couple of nasty bugs in the elaboration process, as well
as in the type inference.

Gave a test case for inference with meta-variables. The variables are not solved yet.