aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Reflection/Equality.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Equality.v b/src/Reflection/Equality.v
index 39d2675b5..d6b7b24fc 100644
--- a/src/Reflection/Equality.v
+++ b/src/Reflection/Equality.v
@@ -1,5 +1,6 @@
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.FixCoqMistakes.
Section language.
Context (base_type_code : Type)