From dd9ba6c1ef9f7e77ae51e9e45fa53c099d92dcff Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Apr 2017 01:25:10 -0400 Subject: Export ClearAll in Tactics --- src/Util/Tactics.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index a54982a17..bab3daf75 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -2,6 +2,7 @@ Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.Tactics.BreakMatch. Require Export Crypto.Util.Tactics.ChangeInAll. +Require Export Crypto.Util.Tactics.ClearAll. Require Export Crypto.Util.Tactics.ClearDuplicates. Require Export Crypto.Util.Tactics.Contains. Require Export Crypto.Util.Tactics.ConvoyDestruct. -- cgit v1.2.3