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.