aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Heaps.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Heaps.v')
-rw-r--r--lib/Heaps.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/Heaps.v b/lib/Heaps.v
index 65334a38..2a21f88c 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -21,6 +21,7 @@
(If an element is already in a heap, inserting it again does nothing.)
*)
+Require Import FunInd.
Require Import Coqlib.
Require Import FSets.
Require Import Ordered.