Jason Gross

> Yes, we could restrict the redundant-& optinization to uint8+, but could we remove uint1 altogether? Do you remember why/when we added it in the first place? I think we...

It would, but I don't have time to prepare an actual fix right now, and this is an easy patch to revert when a fix lands, and I don't think...

> Wouldn'it it be nicer to have an actual fix instead? It seems there are a bunch of fixes for this in the wild that have not been turned into...

> Or it kind of does, but like the second time you press the shortcut? This seems like it adds unnecessary friction. Seems fine to make this behavior configurable, but...

> but the 3-limb version is still stuck on an if with a trivially true condition, u64 < 2^64. https://gist.github.com/andres-erbsen/afdb742c2d400e12b1df24d919cbb722 I will try iterating interleaved bounds-analysis and rewriting next. I...

Here is one issue I've seen (trying to insert prediction on github textbox): Note that this failure mode borks textbox entry on the page, which is a particularly egregious failure...

Longer version:

Note that this issue is also cross-page: if I encounter this error mode on the github page, this prevents fatebook predictions from working in other tabs. If I then refresh...

This seems like it might be a bug in Coq. @herbelin? Also, I'm confused why `intros [Hx [Hy | Hy ] | Hx [Hy | Hy] ]` would have stopped...

> @JasonGross I did coqutil and fiat-crypto is now fine, please have a look to coqtools coqutil still seems to be failing on CI here though? I hope https://github.com/JasonGross/coq-tools/pull/202 will...