GitLab

The closing delimiter in records and arrays is now correctly indented.

The final [end] in a signature or structure should now be correctly
indented. :-)

This guarantees the absence of name clashes.

This guarantees the absence of name clashes.

cannot be generated because the type of some nonterminal symbol is unknown.

Replaced a few redundant tests [if Settings.table then ...]
with assertions [assert Settings.table].

Renamed to [listif] and [elementif].

  defined at different places in the generated file (in order to avoid
  name clashes, and for clarity).

The type env no longer needs to be parameterized.
This makes the API safe (and simpler).
There a slight runtime cost (e.g., from 4.6s to 4.7 seconds).

This seems to cause roughly a 10% speed loss (e.g. from 4.3 to 4.6 seconds).
The current interface is not satisfactory, as it allows the user to
manufacture a continuation that will break our invariants and lead
to a crash.

Added links to CompCert's github repository.

Spell-checking.

['a lr1state -> 'a symbol] and maps a state (an abstract datum)
to (a code for) its incoming symbol. This allows inspecting the
semantic values stored in the stack.
Updated the demo [calc-incremental] to display the contents of
the stack at every token. It seems to work!