Pierre-Marie Pédrot comments

Results 661 comments of


                                            Pierre-Marie Pédrot

Keep objects survive functors and module types

It works though (TM).

Rely on the HConstr machinery also for opaque proofs containing side-effects

@coqbot bench

Rely on the HConstr machinery also for opaque proofs containing side-effects

Clearly very efficient on some extreme examples from fiat-crypto and VST!

Rely on the HConstr machinery also for opaque proofs containing side-effects

No, at least for VST I profiled what was going on an a good part was due to weak sets being inefficient.

Cleanup checker/values after removal of vio (notably: remove Proxy) + votour add vmlibrary to known segments

I think this is going the wrong way, actually: we should use proxy more and rely less on cyclic values for recursive types.

Cleanup checker/values after removal of vio (notably: remove Proxy) + votour add vmlibrary to known segments

@coqbot run full ci

Cleanup checker/values after removal of vio (notably: remove Proxy) + votour add vmlibrary to known segments

@coqbot merge now

Fix the documentation of the typing rules of shifts + a bug in popn

@coqbot run full ci

Fix the documentation of the typing rules of shifts + a bug in popn

After discussing with @yannl35133 we're waiting for a proper proof in metacoq to double-check that everything is fine. The current status of the issue is twofold: - The documentation of...

Fix the documentation of the typing rules of shifts + a bug in popn

@coqbot run full ci