1 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/remake_tactics.sh b/src/Util/remake_tactics.sh
new file mode 100755
index 000000000..69e94cc0b
--- /dev/null
+++ b/src/Util/remake_tactics.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+cat > Tactics.v <<EOF
+(** * Generic Tactics *)
+Require Export Crypto.Util.FixCoqMistakes.
+EOF
+FILES="$(cd Tactics; git ls-files '*.v')"
+for i in $FILES; do
+    echo "Require Export Crypto.Util.Tactics.${i%.v}." >> Tactics.v
+done