GitLab

Menhir 20151112 can, in fact, be used to compile Why3. The actual issue
was that the error reporting module depends on Menhir's table-based
backend, which requires menhirLib. So, the latter is no longer an optional
dependency.

Detect and push down the VC explanations during introduce_premises.

These names are only visible under "ensures" but not under "returns".
If the result is named, the special variable "result" is not used.
In a tuple, either each component should be named, or none at all.
Underscores are allowed. Parentheses around the return type are required.
Each name must be given its own type: "f () : (x y: int)" is rejected.
Identifiers without cast are treated as types, not as names.
To name the result without giving its type, use "returns".

this is much closer now to TAOCP, vol 2, exercise 6 page 7

Black on red was not readable. Colors to be decided.

As a side effect, this also modifies reflection.ml accordingly.