Stéphane Glondu <glondu@debian.org> writes: This is not acceptable to me. [...] I don't fully agree, but I see your point. I suggest to wait then with prooftree until Coq 8.4 enters testing. Bye, Hendrik