#385 (Aug 5, 2017, 12:50:11 AM)

1. merged (detail / hgweb)
2. more horrible proofs disentangled (detail / hgweb)
3. tuned (detail / hgweb)
4. more structural sharing between common target Generic_Target.init (detail / hgweb)
5. exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements (detail / hgweb)
6. treat exit separate from regular local theory operations (detail / hgweb)
7. provide explicit variant initializers for regular named target vs. almost-named target (detail / hgweb)
8. prefer explicit datatype over implicit sum;
   given up separate implementation to pretty-print locale specifications (detail / hgweb)
9. compactified output (detail / hgweb)
10. lifting setup for char (detail / hgweb)
11. one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy (detail / hgweb)
12. uniform namespace handling for both concrete and abstract types, following 32e0da92c786 (detail / hgweb)
13. clarified (detail / hgweb)
14. corrected slip (detail / hgweb)
15. tuned (detail / hgweb)
16. work around weakness in export calculation when generating OCaml code (detail / hgweb)
17. tuned (detail / hgweb)

Started by an SCM change

This run spent:

• 9.8 sec waiting;
• 1 hr 19 min build duration;
• 1 hr 20 min total from scheduled to completion.