Matthieu Sozeau

I pushed a patch that changes the semantics by allowing to identify instances of metas ignoring universes in Ltac, but that might have unforeseen consequences. [constr_eq] does not ignore them,...

That's an interesting report, will look into it!

I've not had a chance yet. The usual suspect is lack of template-polymorphism, but it's unlikely to raise that error a priori. Maybe run_parse_module is using some fancy feature? It...

It does not seem reasonable to me to not fix it so that the firstorder issue stays in the CI. @ppedrot It should be easy to make a specific test-case...

Thanks @mrhaandi !

@coqbot run full ci

@coqbot bench

Slowdowns seem to be mostly related to setoid rewriting

@coqbot bench

@coqbot bench