aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Named/IdContext.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Named/IdContext.v')
-rw-r--r--src/Compilers/Named/IdContext.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Compilers/Named/IdContext.v b/src/Compilers/Named/IdContext.v
index 5ed1e7cf2..d82740cb4 100644
--- a/src/Compilers/Named/IdContext.v
+++ b/src/Compilers/Named/IdContext.v
@@ -1,4 +1,6 @@
+Require Import Coq.Lists.List.
Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Compilers.Named.Syntax.
Section language.