From 0def5869cd18e9d276bb01dfaec56139b1c48b0d Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Tue, 19 Sep 2017 18:22:22 +0200 Subject: [PATCH] Quickfix --- FiniteSets/FSets.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FiniteSets/FSets.v b/FiniteSets/FSets.v index c7d000a..6c66da7 100644 --- a/FiniteSets/FSets.v +++ b/FiniteSets/FSets.v @@ -1,2 +1,2 @@ Require Export HoTT HitTactics. -Require Export kuratowski_sets kuratowski.operations kuratowski.properties extensionality. \ No newline at end of file +Require Export kuratowski_sets kuratowski.operations kuratowski.properties extensionality prelude.