Commit 59c3c754 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Changes.g

parent af37e557
Pipeline #84193 passed with stages
in 26 seconds
# Changes
## 2019/06/22
* Fix compatibility with Coq 8.7 and Coq 8.9:
- In Coq 8.7, in the syntax { x : T & T' } for the sigT types,
it was not possible to omit the type T.
- An anomaly in Coq 8.7 has been worked around.
- In Coq 8.9, the numeral notation for positives moved from
Coq.Numbers.BinNums to Coq.PArith.BinPos.
## 2019/06/13
* The Coq development is now free of any axiom (it used to use axiom
......
Supports Markdown
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