Jean-Christophe Léchenet
Jean-Christophe Léchenet
Still being polished
I had the same bug with [Jasmin](https://github.com/jasmin-lang/jasmin), without `--working-dir`. `opam install . --deps-only` at the root does not install `coq-mathcomp-algebra` (among others), and moreover does not report the package as...
If there is no conflict, this probably means that the bank is empty, so another fix could be to check if the set of conflicts is empty.
One advantage of allowing that could be to be more strict about const arrays. For instance, for now, we allow to write `r = g`, where `r` is a `reg...
(While writing that, I realize it is not clear in my mind if `const` means that `r` is a constant pointer, a pointer to constant arrays, or both.)
For now, we reject both `r = s` and `r[i] = ...`. Maybe we should just reject the latter.
I have a branch somewhere, let me resurrect it.
I have just rebased the branch: `subarray_unknown_index`. @defund I know the branch is a bit buggy, but please try it and report whether it suits your needs or if it...
Ping @defund. Have you tried the branch?
Compiling with `coqc -async-proofs on` also triggers the anomaly.