summaryrefslogtreecommitdiff
path: root/test-suite/ide/blocking-futures.fake
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/ide/blocking-futures.fake')
-rw-r--r--test-suite/ide/blocking-futures.fake1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
index b63f09bc..541fb798 100644
--- a/test-suite/ide/blocking-futures.fake
+++ b/test-suite/ide/blocking-futures.fake
@@ -4,6 +4,7 @@
# Extraction will force the future computation, assert it is blocking
# Example courtesy of Jonathan (jonikelee)
#
+ADD { Require Coq.extraction.Extraction. }
ADD { Require Import List. }
ADD { Import ListNotations. }
ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. }