Pierre-Marie Pédrot comments

Results 661 comments of


                                            Pierre-Marie Pédrot

faster PCUICSR

Note that coq/coq#19126 has probably made this PR much less usefull in practice.

Faster composed module substitution of terms.

@coqbot bench

Faster composed module substitution of terms.

It actually helped on the compcert example.

Faster composed module substitution of terms.

I think that the bench basically doesn't measure anything coqchk-related. The current run is just noise. But on the one-liner from compcert this PR reduces the coqchk invocation from ~87s...

Fix incorrect handling of Elimination and Case schemes

@coqbot run full ci

Fix incorrect handling of Elimination and Case schemes

CI failure unrelated, let @coqbot merge now

Add convenience API Sorts.make taking quality and universe

@coqbot run full ci

Add convenience API Sorts.make taking quality and universe

@coqbot merge now

Do not rely on floating universes in the upper layers

The CoqHammer backwards compatible overlay has been merged, this is ready to go.

Do not rely on floating universes in the upper layers

@coqbot run full ci