Document (some) Proof using syntax + the new Optimize commands
Removing yet another source of remaining local definitions.
Move conjugate_verb_to_be next to cString.plural.
Fixing Scheme Equality, after bug introduced in bf018569405c.
Preserving the good effect of 014e5ac92a on not leaving dangling local
definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).
Reproduction cases for the test suite.
Add missing "Fail" to test case for bug #2814.
Get rif of exit codes 120, 121, 123, and 124.
Exit with code 129 when an anomaly occurs.
Use return code to classify anomalies as active open bugs.
Adding a terminal library.
Adding a pretty-printing style library.
Plugging the color initialization in the Coqtop loop.