From 838aef543b748bc9221cd0971c4e6d6714c139df Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Sun, 15 Oct 2023 10:22:47 +0200
Subject: [PATCH] FiniteTypes: Fix build on coq v8.12 to v8.14

The file `FiniteTypes.v` did import `Cardinals` from `ZornsLemma`.
But with coq v8.12 to v8.14, when building in parallel, the dependency
is misinterpreted to mean the file
`theories/ZornsLemma/Cardinals/Cardinals.v` instead of
`theories/ZornsLemma/Cardinals.v`. For this reason, building using the
affected versions caused build failures, because some lemmas were
undefined.

For this reason, this patch lists the imports of `FiniteTypes.v` with
their full path and does not depend use
`theories/ZornsLemma/Cardinals.v`.

Interestingly, before this patch, if the file
`theories/ZornsLemma/Cardinals.vo` was compiled before `FiniteTypes.v`
was processed, then the right file would be chosen and it would work.
---
 theories/ZornsLemma/FiniteTypes.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/ZornsLemma/FiniteTypes.v b/theories/ZornsLemma/FiniteTypes.v
index c946590c..a634a6c8 100644
--- a/theories/ZornsLemma/FiniteTypes.v
+++ b/theories/ZornsLemma/FiniteTypes.v
@@ -6,7 +6,9 @@ From Coq Require Import
   Lia
   Program.Subset.
 From ZornsLemma Require Import
-  Cardinals
+  Cardinals.Cardinals
+  Cardinals.Combinatorics
+  Cardinals.CSB
   DecidableDec
   FiniteImplicit
   Finite_sets