Remove tactic hresolve_core

[SkySkimmer]

The implementation is fragile due to being based on detyping and a loc hack, and it seems unused.

It was also not in the doc until
#16498 (8.17) and then only got a doc stub.

Overlays:

• Adapt to coq/coq#17035 (remove hresolve) snu-sf/paco#47 (note this is just a removal of unused tactic definitions)

[SkySkimmer]

@coqbot run full ci

[JasonGross]

According to #16846 it is used to implement hpattern which looks like a useful tactic that I'd be interested in seeing upstreamed into Coq rather than broken

[SkySkimmer]

@coqbot run full ci

[coqbot-app]

🔴 CI failure at commit fd455be without any failure in the test-suite

✔️ Corresponding job for the base commit 41e76f5 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-paco

• You can also pass me a specific list of targets to minimize as arguments.

[Zimmi48]

Given why hresolve_core was introduced, I don't think it should be removed without hget_evar being removed at the same time.

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: Please take care of the following overlays:

• 17035-SkySkimmer-no-hresolve.sh

[herbelin]

According to #16846 it is used to implement hpattern which looks like a useful tactic that I'd be interested in seeing upstreamed into Coq rather than broken

Ideas from hresolve_core were used in destruct (via Evarconv.second_order_matching). I don't remember the exact differences between Evarconv.second_order_matching and hresolve_core, but for sure, these are ideas to valorize and to develop further. Iirc, Matthieu was working on generalizing the use of Evarconv.second_order_matching as part of Unifall, but, again, I don't know the exact status of it.