#968 (Jul 24, 2019, 1:14:34 AM)

1. treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation); (detail / hgweb)
2. discontinued Proofterm.Promise (cf. 725438ceae7c); (detail / hgweb)
3. clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
   added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof; (detail / hgweb)
4. tuned comments; (detail / hgweb)
5. proof terms are always constructed sequentially;
   discontinued unused Proofterm.Promise -- too complex; (detail / hgweb)

Started by an SCM change

This run spent:

• 24 min waiting;
• 1 hr 22 min build duration;
• 1 hr 46 min total from scheduled to completion.