Pierre-Marie Pédrot

More efficient compilation of PArray blobs in the VM.

4

We store persistent arrays whose elements are all structured values as a single structured value, and copy the resulting blob at runtime to generate a fresh persistent array.

It was missing a closing parenthesis. For readability I turned this into braces instead.

Remove the cutrewrite tactic.

3

It was deprecated since Coq 8.5.

Algorithmically faster computation of argument scopes.

2

Instead of using the naive reduction algorithm from Reductionops, we rely on kernel reduction as this one features delayed substitution. This prevents an exponential blowup in presence of nested let...

Inefficient computation of argument scopes

1

The computation of implicit arguments uses an inefficient reduction algorithm to expose telescopes. This is very bad in presence of nested let-ins, as it results in an exponential behaviour. Original...

[CoqIDE] Display warnings in their own tab.

5

Follow-up of #19188. It was annoyingly confusing to get the warnings in the error tab, as it seemed to indicate that the file was not properly compiling.

Do not create global constraints for applied template polymorphic types

98

This is a partial step towards coq/ceps#90. Backwards compatible overlays: - https://github.com/jwiegley/category-theory/pull/147 - https://github.com/JasonGross/neural-net-coq-interp/pull/62 - https://github.com/mit-plv/fiat-crypto/pull/1933 - https://github.com/PrincetonUniversity/VST/pull/787

This test is extracted from Mtac2 and fails on master, but is solved by #19228. ```coq Require Coq.Lists.List. Import Coq.Lists.List. Import ListNotations. Class MBind (M : Type -> Type) :=...