#901 (Mar 27, 2019, 12:50:07 AM)

1. merged (detail / hgweb)
2. more informative Spec_Rules.Equational, notably primrec argument types; (detail / hgweb)
3. clarified signature: avoid direct comparison on type rough_classification; (detail / hgweb)
4. tuned proofs; (detail / hgweb)
5. removed spurious debugging; (detail / hgweb)
6. export propositional status of consts; (detail / hgweb)
7. merged (detail / hgweb)
8. generalised homotopic_with to topologies; homotopic_with_canon is the old version (detail / hgweb)
9. follow up on Braun: get timing function right (detail / hgweb)
10. Tweak Braun tree list_fast_rec recursion.
    
    A minor adjustment simplifies the termination argument slightly. (detail / hgweb)

Started by an SCM change

This run spent:

• 5.8 sec waiting;
• 1 hr 13 min build duration;
• 1 hr 13 min total from scheduled to completion.