* Replace various instances of output and finishOutput by an OutputManager trait.

* Simple Propositional solver (trivial) now can accept arbitrary number of premises.
Correction of many bugs related to the propositional solver,
and a crash in the kernel proof checker when using LeftOr and RightAnd on empty premises.

* Ongoing work on error reporting

* Rewrite tactic system: Proof syntax comes with Theorem environment, not with Library.
Purged Library from old implementation. Translated WithProofs to WithTheorems.
Adapted ProofSteps: They depend directly on a given proof
Ongoing adaptation of BasicProofSteps

* More work on theorems and proof. Proof steps and intermediate representations depend on a specific proof given as parameter. They should be type members instead?
THM uses a context function. This allows to make proofcontext elements available only there.

* Ongoing work on writing theorems. Use refinement types instead of type parameters, much more adequate and less boilerplate.

* Re-did theorem interface with sourcecode (macro)
Repaired existing proof tactics

* Finished to adapt old proof rules. Managed subproofs.
The InnerProof class is now an inner class of the proof abstract class, using dependent path instead of type parameter.
Subproofs essentially implemented.
Proof steps get the correspondance between facts and integeres as late as possible to allow delaying of importing and computing the
positions of the facts in the surrounding proof, so that the inner peoof does not influence the outer proof until the very last moment.
More.

* rehabilit Discharge

* Printer for higher proofs.

* Revamp LisaException. (Untested)

* Moved ProofTacticJudgement to inner classes of proofs because projection types are buggy/limited
Proof Tactics now return a list of proof steps and a list of premisces. Constructing the SCSubproof is left to the ProofStep creation.
Premises are now not members of Proof Tactics: Can be computed. Instead, there should be a mix of "user given" premises and arbitrary premises (theorems...)
More that I don't remember.
Not working at this stage.

* Full overall of tactic system. Soon finished, couple of point to fix.

* Finished the system of tactics completely, found workarround for weird bevaviour and bugs of dotty.
Adapted most existing tactics, only instantiation ones left.

* Just left with overloading issues on proof helpers (by, ...)

* Everything seems to work. All proof steps rehabilited. Much cleaner. Solved all (most?) of the little overloading and ambiguity about which sotty complained.

* Finished tactics and error reporting update