Pierre-Marie Pédrot

Let's merge then @coqbot merge now

@coqbot merge now

@coqbot run full ci

@coqbot bench

@coqbot bench

@coqbot bench

At the call we discussed the *sea snake* idea of clever fixpoint refolding, but this was motivated by user-friendliness. This PR is rather an experiment to assess the potential performance...

This PR makes Equations loop on a function ominously annotated with the comment "(** Now we define an obviously non-terminating function. *)"... There is probably some progress issue somewhere when...

This doesn't look like a great idea in the end. It's slower on some devs, and there is some completeness issue it seems.

> That conversion is less efficient with refolded fixpoints? Unclear to me. I think we need more experiments. > That unguarded fixpoints, or at the least the one in Equations,...