From 9765692cdc24a1ad4fe86320df7dc288b4d1d86d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 10 Oct 2018 10:15:18 -0400 Subject: Export more tactics in Tactics.v --- src/Util/Tactics.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Util') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 95b4a29fc..cd045fdbb 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -20,6 +20,7 @@ Require Export Crypto.Util.Tactics.Forward. Require Export Crypto.Util.Tactics.GetGoal. Require Export Crypto.Util.Tactics.Head. Require Export Crypto.Util.Tactics.MoveLetIn. +Require Export Crypto.Util.Tactics.NormalizeCommutativeIdentifier. Require Export Crypto.Util.Tactics.Not. Require Export Crypto.Util.Tactics.OnSubterms. Require Export Crypto.Util.Tactics.PoseTermWithName. -- cgit v1.2.3