Commit 6cefed83 authored by POTTIER Francois's avatar POTTIER Francois

Cosmetic fixes in the change logs.

parent 3df9c52f
Pipeline #82983 failed with stage
......@@ -16,7 +16,7 @@
remains undocumented. (Reported by kris.)
* Coq back-end: multiple changes to stay up-to-date with respect to
coq-menhirlib. See `CHANGES.md` there.
coq-menhirlib. See [coq-menhirlib/CHANGES.md](coq-menhirlib/CHANGES.md).
* Coq back-end: the generated parser now contains a dedicated inductive
type for tokens. This removes the need for `Obj.magic` in client code
......
# Changes
## 2019/02/XX
## 2019/06/13
* The Coq development is now free of any axiom (it used to use axiom
K), and the parsers can now be executed directly within Coq, without
`K`), and the parsers can now be executed directly within Coq, without
using extraction.
* The parser interpreter is now written using dependent types, so that
no dynamic checks are needed anymore at parsing time. When running
the extracted code, this should give a performance boost. Moreover,
efficient extraction of int31 is no longer needed. This required
efficient extraction of `int31` is no longer needed. This required
some refactoring of the type of parse trees.
* Instead of being a dependent pair of a terminal and a semantic
values, tokens are now a user-defined (inductive) type.
* Instead of a dependent pair of a terminal and a semantic
value, tokens are now a user-defined (inductive) type.
## 2018/08/27
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment