Rodolphe Lepigre

Add reproduction test case for #10149.

3

Running `DUNE_COQ_TEST=enable ./dune.exe build @minimum-recomp` gives the following on master: ``` File "test/blackbox-tests/test-cases/coq/minimum-recomp.t", line 1, characters 0-0: diff --git a/_build/.sandbox/0d58af7d43c673e8a5a21a2e5756ee3d/default/test/blackbox-tests/test-cases/coq/minimum-recomp.t b/_build/.sandbox/0d58af7d43c673e8a5a21a2e5756ee3d/default/test/blackbox-tests/test-cases/coq/minimum-recomp.t.corrected index 602c8e27b..ee8f4fdd6 100644 --- a/_build/.sandbox/0d58af7d43c673e8a5a21a2e5756ee3d/default/test/blackbox-tests/test-cases/coq/minimum-recomp.t +++ b/_build/.sandbox/0d58af7d43c673e8a5a21a2e5756ee3d/default/test/blackbox-tests/test-cases/coq/minimum-recomp.t.corrected @@ -9,4...

### Description of the problem See [here](https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/Unbearably.20slow.20compilation.20of.20some.20Coq.20files/near/442832199). ### Version of Coq where this bug occurs master