Rao Xiaojia

Great work -- many thanks for the PR! I'll look into them, although I'm not completely sure if I should first merge a version into 1.0 or combine this with...

In fact, your PR makes me think it might be a good idea to create a PR from my 2.0 update fork so that this is visible in the main...

Would you be updating this branch of work to the 2.0 update at some point (be it either just the definitions or with proofs)? That being said, by looking at...

This is for sure a good idea for the long term, especially if at some point in the future I'd no longer be able to maintain this library -- that...

> Since we have resolved #29, feel free to open [an issue](https://github.com/coq-community/manifesto/issues/new?assignees=&labels=move-project&projects=&template=1-move-a-project.md&title=Proposal+to+move+project+X+to+coq-community) about moving the project when you are ready. > > I'd like to emphasize that a move to...

> > I've read the community manifesto and reckon that I'll have to care a lot about backward compatibility after submitting anything there, so I thought it makes sense to...

> @raoxiaojia with #31 merged, what are your plans going forward, would moving to coq-community be advantageous? It surely is the plan! I haven't really been working on anything much...

> @raoxiaojia it was nice to meet in London. What do you think about this one? (One or more of: Platform, Coq CI, coq-community, ... ) > > By keeping...

> I'm currently working on the proof that the Wasm module we generate instantiates. Since you made some changes to the instantiation_spec, I'd like to update to a version of...

> > I'm hoping the definitions should be pretty stable, although proofs down that line haven't been updated, so there might be some mistakes. I'm guessing your line of work...