aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tuple.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Tuple.v')
-rw-r--r--src/Util/Tuple.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index d1e0177f2..b8a5c2738 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -3,7 +3,9 @@ Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Lists.List.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.ListUtil.
Require Export Crypto.Util.FixCoqMistakes.