Yves Bertot

I am sorry for the time you spent on this, but I ignored this issue, because the I have a systematic approach to porting coq-dpdgraph to new releases of Coq,...

We can talk about it the next time we meet (I am currently reading your article BTW).

Yes, PR requests merged as soon as mid august make coq-master incompatible with coq-V8.18.

Making a world map is interesting for communities that have an international spread. In the case of Coq, the development team is small so this may not be the right...

I agree that I would like to have a naming scheme for theorems of real numbers that is closer to the one in Q, Z, or nat, because these have...

Apparently, here we have a problem because we mistake the objective with means to achieve it. You could also choose the term "Boost stdlib development" or something similar. The move...

You have to give information about the compilation setup. What were all the commands you executed to get to this error message?

It seems I made a mistake and `fib 12` does not provoke the problem, rather `fib 14` should be used. But it is still quite a small number. Here is...

Here is the piece of code that is frowned upon (from theories/lebesgue_integral.v) 

I thought I had that part right. The shell I show you in the terminal part of the window has the same path as the shell where the code was...