added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
clarified future scheduling parameters, with support for parallel_limit;
misc tuning and clarification;
more tight treatment of subgoals: main goal may refer to extra variables;
optional proof context for unify operations, for the sake of proper local options;
clarified modules;