Laurent Théry said:
Which tutorial you are talking about. I am trying to maintain upto date version of tutorials here. It works with coq 8.16 and mathcomp 1.16.
It is the Mathematical Components book from Enrico Tassi and Assia Mahboubi.
I suppose the changes come from replacing the usual inheritance by HB, hope there's some tutorial some day!
Raul has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC