Tim Carstens

I should have time this week to reach out and make it happen 👍

@mattam82 Is this still open? I have time to work on this.

#257 might be related, I'm not sure. In that issue, it is reported that vscoq hangs. That's not the case here; here, vscoq works just fine if you specify the...

@MSoegtropIMC I noticed that `coq-vst.opam` and `coq-vst-32.opam` both seem to work. Does that mean this issue can be closed?

I saw the discussion around [coq/coq#12686](https://github.com/coq/coq/issues/12686). I agree with your assessment: the current approach to variants is not ideal, and if Coq is going to support `_CoqProject`, then Coq also...

I think I can offer you some relief re: including `_CoqProject` file in a downloadable example. I've updated [my example](https://gist.github.com/intoverflow/6896430492576d4087cf2709057f67a5) to support `BITSIZE=opam` (and to use this value by default)....

GCC is impacted by this, which means CompCert is also impacted by this. (I confirmed with examples from the "trojan source" repo.) However, I do not believe this is a...

Looping back here to share some updates: 1. The CertiCoq `prims` branch provides support for binding Coq definitions/axioms to C functions. @joom and @zoep have demo code for some `Int63`...

Quick update: I discussed this issue with @zoep , @andrew-appel , and @john-ml earlier this week. We concluded the following: 1. We want `Extract Constants []` to be able to...

Thank you for reaching out @kuruczgy! You happened to catch us while most folks are either on vacation or preparing for the next term at university. We are tracking and...