Skip to content

Commit

Permalink
FiniteTypes: Fix build on coq v8.12 to v8.14
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Columbus240 committed Aug 6, 2024
1 parent 349154f commit 81e95bc
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion theories/ZornsLemma/FiniteTypes.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 81e95bc

Please sign in to comment.