Bad interaction of async proofs and HB

[eponier]

I don't know if it is an error coming from HB or Coq, but the easy way to reproduce it is with HB. Feel free to transfer the bug report to coq if this is more appropriate.

The bug is really easy to reproduce with CoqIDE. Just open the following file and go to the end. The error Anomaly "Uncaught exception Not_found" is produced. I tried coq 8.19 and 8.18, with HB 1.17.

From HB Require Import structures.

Goal True.
Proof. reflexivity.
Qed.

[eponier]

Compiling with coqc -async-proofs on also triggers the anomaly.

[eponier]

Never mind, this is an occurrence of https://github.com/LPCIC/coq-elpi/issues/543, closing.