GeoCoq broken with Coq 8.9 (master)

[Zimmi48]

GeoCoq/Meta_theory/Models/hilbert_to_tarski.v

Lines 208 to 210 in 8ddee16

	Lemma colH_dec : forall A B C, ColH A B C \/ ~ColH A B C.
	Hint Resolve colH_trivial121 colH_trivial122 colH_trivial112 colH_trivial111 colH_permut_231 colH_permut_312 colH_permut_321
	colH_permut_213 colH_permut_132 colH_permut_231 : colH.

This lemma is only proved at the very end of the file. In Coq 8.9, nested lemmas are disabled unless you turn option Nested Proofs Allowed on. So you should either add Set Nested Proofs Allowed at the beginning on this file, or move this lemma's statement to the bottom, right before its proof.

[Zimmi48]

cc @Boutry

[Zimmi48]

BTW this big commit also introduced a dependency on math-comp which is not indicated in the changelog.

[jnarboux]

Thank you for reporting, it was a typo, the nested lemma has been deleted. I added a word about the math-comp dependency in the Changelog.