Replace elimtype False by exfalso

[yforster]

@SkySkimmer this should fix Coq master again

[yforster]

I accidentally changed the CI to use coq-8.18 in this merge, that's why we didn't catch the incompatibility with Coq master -- now that's fixed as well

[JasonGross]

The opam files also need to be updated, eg,

metacoq/coq-metacoq-utils.opam

Line 32 in adc980c

"coq" { >= "8.18" & < "8.19~" }

needs to permit dev

[yforster]

Thanks @JasonGross!

[yforster]

Still erroring in CI, but I think this error we've had before my merge as well? Good to merge into main @SkySkimmer?

[SkySkimmer]

I don't know why you're asking me tbh

[JasonGross]

I think this should be merged. I expect MetaCoq to still fail on Coq master with this universe error on vos mode, which I think is possibly a regression Coq-side. MetaCoq
CI side this can be fixed by disabling vos for whichever component is failing, which I seem to recall having to do for some part of quotation already.

[JasonGross]

Ah, the change I had already made was

metacoq/Makefile

Line 103 in adc980c

$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent

in

metacoq/Makefile

Lines 84 to 106 in adc980c

	vos:
	$(MAKE) -C utils
	$(MAKE) -C common
	$(MAKE) -C template-coq
	$(MAKE) -C pcuic vos
	$(MAKE) -C safechecker vos
	$(MAKE) -C template-pcuic vos
	$(MAKE) -C quotation vos
	$(MAKE) -C erasure vos
	$(MAKE) -C erasure-plugin vos
	$(MAKE) -C translations vos
	quick:
	$(MAKE) -C utils
	$(MAKE) -C common
	$(MAKE) -C template-coq
	$(MAKE) -C pcuic quick
	$(MAKE) -C safechecker quick
	$(MAKE) -C template-pcuic quick
	$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent
	$(MAKE) -C erasure quick
	$(MAKE) -C erasure-plugin quick
	$(MAKE) -C translations quick