Update documentation
A non-exhaustive list of sections that are not up-to-date.
High priority (for 1.4.0)
-
9.4. Isabelle/HOL: needs update to isabelle 2019 -
10.6. Proof Strategies: needs update to auto levels 0 to 3 -
document foreach
-
document micro-C and micro-python (at least short paragraphs refering to the web pages) -
document old and at (@filliatr ) -
document auto-dereference
Medium priority (as soon as possible)
-
7.5.2. Record types: in particular the differences between abstract/private and such, and the type invariants -
7.5.6. Module Cloning: to be completed -
4.11. Infering loop invariants: needs porting from latex to rst (@marche ) -
Functor extraction (@mariojppereira )
Low priority
-
7.5.1. Algebraic types -
mutually recursive types and functions
-
-
7.6. Standard Library: expand and add more modules there -
Cursor -
Seq
-
-
document termination/variant/etc. -
fix undefined labels and multiply-defined labels in Latex version. This seems to be a bug in sphinx, in its modules for formal grammars, which produces labels from non-terminal by replacing the underscore characters by minus, but not always. We can wait Sphinx to be fixed, or stop using underscores in non_terminals (annoying)