Pierre-Marie Pédrot

@coqbot ci minimize

Nitpicking the nomenclature, but the real need for this PR is rather an independent fix than an overlay. Coq-elpi is currently playing fast and loose with evarmaps and it happens...

I'd still support inclusion of this PR. It's sound and removes a todo, even though the frequency of occurrences of match nodes in usual goals is null.

@Janno if you want to make progress on this PR, I'd recomment splitting it into subPRs, especially the Hint Extern part should be implemented separately.

It's easy to backport the change that makes nf_evar explode on dangling evars, if that helps you.

This particular bug seems to have been fixed on coq-elpi master (by #581 most likely). The test-suite still fails with an anomaly on undefined evars though. I'll try to minimize...

I am very confused now: the same reduced example still triggers an anomaly when it is compiled from within the test folder of tc-elpi, but not when launched from the...

@gares this [seems to be failing](https://gitlab.inria.fr/coq/coq/-/jobs/4300288) but I do not understand why. I get ``` Error: Destructing let on this type expects 2 variables. ``` in some elpi test but...

Indeed, there is some trickery involved in detyping. I ended up emulating the old behaviour through an explicit registering in the upstream PR. @gares tell me if you're fine with...

Note that I think we are missing half of the tools for this. The option prevents the *caller* from depending on hints that were not required, but there is no...