Matthieu Sozeau

I’m surprised you couldn’t do it with fuel and a computed bound, as there is a finite number of references in a global_environment + term. Termination might be tricky, e.g....

@CohenCyril any news on this front?

There's a printing function in `extraction/test-suite/Test.v` that could be migrated to `Ast.term` easily I guess. Just to be clear, you're debugging the implementation, not a proof about it, right? Also,...

Indeed, that's a bug in the Derive code, still to investigate. However, for vectors you shouldn't need that instance, the default dependent eliminator of vectors produced by Coq is enough.

Yes, “simp” generates an unconditional equation for the second clause while rewriting with it should really depend on the conditional “le_lt_dec y x”. If you use a “with” clause instead...

One way to fix this would be to generate conditional equations in that case

I could at least warn if there is a recursive call under a match in an equation, it’s an easy syntactic check.

@Tdiazt that looks unrelated. It’s probably autorewrite looping for another reason. Can you try rewriting with the equations (queries_size_equation_1 and so on) to understand how it could loop?

It might be because `simp f` calls also `typeclasses eauto with f Below subterm_relation rec_decision`, where `f` represents the hint database associated to `f`. (Print HintDb f to see its...

Indeed there's a bug in the graph construction here.