Jason Gross

I guess coqbot doesn't listen to comments on this repo, so running minimization at https://github.com/coq-community/run-coq-bug-minimizer/issues/2#issuecomment-2417648469

@mkarup what version of Coq are you using? There are no versions of coq-certicoq and coq-wasm on opam that are compatible with the same Coq versions.

Here is a somewhat reduced test-case, that depends only on the Declare ML Module "coq-certicoq.plugin". and on compcert.lib.Integers (still working on working around AbsInt/CompCert#526) ```coq (* -*- mode: coq; coq-prog-args:...

I don't suppose there's a way to bypass `CertiCoq Compile` and replicate the same anomaly with just MetaCoq commands?

And here's a version that depends only on Declare ML Module "coq-certicoq.plugin". ```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums"...

The codecon site is available on the web archive (http://web.archive.org/web/20110613194315/http://www.codecon.org/2006/), maybe you want to link there?

I could not find the slides in git history. The link seems to have been added at https://github.com/dsw/delta/commit/e487c1c12fecab44d3d5c598161b2e402f42c060 without the sides being added at the same time, and without the...

Sorry it took me so long to get back to you. On looking at things again, I think monoids are already enough to give intrinsic typing (the DTM abstraction needs...

What is the benefit of having primitive strings over using `array int`? The downside I'm concerned about is ad-hoc complication of the kernel and tcb. (If the primary upside is...

What is the status of Fiat Crypto Legacy?