From 30fe1f7ee6485ec1ea359701c7c05f45978a280b Mon Sep 17 00:00:00 2001 From: Columbus240 <8899730+Columbus240@users.noreply.github.com> Date: Fri, 20 Aug 2021 01:54:19 +0200 Subject: [PATCH] Fix compilation on v8.10 --- theories/ZornsLemma/Families.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/ZornsLemma/Families.v b/theories/ZornsLemma/Families.v index b9707eed..3bdbfd7e 100644 --- a/theories/ZornsLemma/Families.v +++ b/theories/ZornsLemma/Families.v @@ -1,10 +1,9 @@ From Coq Require Import Classical_Prop. From Coq Require Import Classical_sets. -From Coq Require Export Ensembles. -From ZornsLemma Require Import EnsemblesImplicit. From ZornsLemma Require Export EnsemblesSpec EnsemblesTactics. From ZornsLemma Require Import Image ImageImplicit. - +From ZornsLemma Require Import EnsemblesImplicit. +From Coq Require Export Ensembles. Set Implicit Arguments. Section Families.