Anton Trunov

Related issue: #900

Thank *you*! I appreciate your words very much. Your version is really nice! And thanks for the exercise :) > I think the fist lemma should be a PR on...

Here is an analogous Coq function that is considered total: ```coq From Coq Require Import List. Inductive Tree := Branches : list Tree -> Tree | Node : nat ->...

On top of everything said I can add that I don't mind having a special place (a dedicated GitHub organization or something like that) for paper artifacts or adding badges...

I wouldn't oppose removing coq-bits from opam. I added it there just because it used to be on opam.

Hi @strub! @volodeyka and I could give you a hand with porting certicrypt to Coq 8.11 as part of @volodeyka's internship project. Please let us know if it works for...

@palmskog Thanks for the pointer!

> We can enforce this with GitHub but then it won't allow pushing commits directly even for trivialities (which may be fine). I'm in favor of going through PRs even...

@Zimmi48 I think your proposal makes total sense. We can always tweak some details as we go along, right?

I also just ran into this. Thanks for the cool tool!