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: Jul 25 2024 at 16:02 UTC