TODO

* fix ex & all without dot
* update 'thesis' in *-intro
* intros, forall-intros, impl-intros
* make lemmas etc work with modules

* more logic: induction, sets, etc
* tauto & auto tactics
* lambda correction (correct_lambda etc.) is quadratic, which slows
  down the parser unacceptably
* bug: nested modules don't quite work
* forward bug (checking frames does not work)
* bug: forward should be disallowed in macro functions (check if this is so)
* macro invocation stacktrace
* fix the `tactic' and `rule' macros as they are very inefficient
  and do not work with partial application
* replace (a = b) with (equal A a b) during parsing, with an inferred
  type A; report error if the type cannot be inferred

* 'mark' is a stupid hack which doesn't fully work and should be removed
* fix comparing & matching recursive data structures
* Better (O(1)) logic variable handling in fix etc.

* names should be preserved for variables in fix etc
* Get rid of quadratic time in join-tokens -- improve token list representation.
* CAppl
* inherit Module
* improve efficiency of type inference
* macro priorities instead of syntax macrosep
* saving parsed files in binary (*.hcpb)
* Improve evaluator efficiency even more
* Improve quoted match / equal efficiency
* In the parser, translate closed lets directly into Delayed nodes (?)
* Type inference (fun macro)
* Improve Node.to_string (use pretty printing from the ocaml's Format module)
* lazy matching
* 'syntax drop' for blocks and macroseps