Commit 206abba6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Update changes.

parent 70ddd069
Pipeline #65229 passed with stages
in 1 minute and 56 seconds
......@@ -15,6 +15,17 @@
must be used instead. The switch `--only-preprocess-for-ocamlyacc`
remains undocumented. (Reported by kris.)
* Coq backend: multiple change to stay up-to-date with respect to
coq-menhirlib. See its corresponding file.
* Coq backend: The generated parser now contains a dedicated inductive
type for tokens. This prevents the use of Obj.magic in client code
when the parser is used via extraction.
* Coq backend: The generated parser checks that the version of
MenhirLib matches. This check can be disabled with
## 2018/11/13
* In `.mly` files, a new syntax for rules has been introduced, which is
......@@ -12,6 +12,9 @@
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.
## 2018/08/27
* Avoid an undocumented mode of use of the `fix` tactic,
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