Commit 0c125b92 authored by POTTIER Francois's avatar POTTIER Francois

parent 496b9bec
# Changes
## 2018/10/31
## 2018/11/06
* In the Coq back-end, avoid pattern-matching at type `int31`,
which will disappear in future versions of Coq.
Instead, convert `int31` to `Z`, and perform pattern matching in `Z`.
(Reported by Vincent Laporte, implemented by Jacques-Henri Jourdan.)
* Implement a more economical renaming scheme for OCaml variables
during the elimination of `%inline` symbols. This leads to slightly
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