More fine-grained tactics imports

10 files changed, 25 insertions, 18 deletions

diff --git a/src/Arithmetic/Karatsuba.v b/src/Arithmetic/Karatsuba.v
index 59dcc5108..d7b988e17 100644
--- a/src/Arithmetic/Karatsuba.v
+++ b/src/Arithmetic/Karatsuba.v
@@ -1,6 +1,6 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Algebra.Nsatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.LetIn Crypto.Util.CPSUtil Crypto.Util.Tactics.
+Require Import Crypto.Util.ZUtil Crypto.Util.LetIn Crypto.Util.CPSUtil.
 Require Import Crypto.Arithmetic.Core. Import B. Import Positional.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.IdfunWithAlt.
@@ -200,4 +200,4 @@ Context (weight : nat -> Z)
   Qed.
 End Karatsuba.
 Hint Opaque goldilocks_mul : uncps.
-Hint Rewrite goldilocks_mul_id : uncps.
\ No newline at end of file
+Hint Rewrite goldilocks_mul_id : uncps.
diff --git a/src/Arithmetic/ModularArithmeticPre.v b/src/Arithmetic/ModularArithmeticPre.v
index ae27b290f..0dc8162b2 100644
--- a/src/Arithmetic/ModularArithmeticPre.v
+++ b/src/Arithmetic/ModularArithmeticPre.v
@@ -4,6 +4,7 @@ Require Import Coq.Logic.EqdepFacts.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.NumTheoryUtil.
 Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Tactics.BreakMatch.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
   symmetry.
diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v
index 842313b93..a4305a849 100644
--- a/src/Arithmetic/PrimeFieldTheorems.v
+++ b/src/Arithmetic/PrimeFieldTheorems.v
@@ -12,6 +12,7 @@ Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Require Crypto.Algebra.Hierarchy Crypto.Algebra.Field.
 
 Existing Class prime.
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
index e84c8d083..7ff86258c 100644
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ b/src/Arithmetic/Saturated/MontgomeryAPI.v
@@ -10,12 +10,13 @@ Require Import Crypto.Arithmetic.Saturated.Wrappers.
 Require Import Crypto.Arithmetic.Saturated.AddSub.
 Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil.
 Require Import Crypto.Util.Tuple Crypto.Util.LetIn.
-Require Import Crypto.Util.Tactics Crypto.Util.Decidable.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.Zselect.
 Require Import Crypto.Util.ZUtil.AddGetCarry.
 Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.Tactics.UniquePose.
 Local Notation "A ^ n" := (tuple A n) : type_scope.
 
 Section API.
diff --git a/src/Demo.v b/src/Demo.v
index fc048d051..2011fcb0d 100644
--- a/src/Demo.v
+++ b/src/Demo.v
@@ -1,22 +1,22 @@
 (* Following http://adam.chlipala.net/theses/andreser.pdf chapter 3 *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz.
-Require Import Crypto.Util.Tactics Crypto.Util.Decidable.
+Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable.
 Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
 Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
 Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
 Import ListNotations. Local Open Scope Z_scope.
-    
+
 Definition runtime_mul := Z.mul.
 Definition runtime_add := Z.add.
 Delimit Scope runtime_scope with RT.
 Infix "*" := runtime_mul : runtime_scope.
-Infix "+" := runtime_add : runtime_scope. 
+Infix "+" := runtime_add : runtime_scope.
 
 Module Associational.
   Definition eval (p:list (Z*Z)) : Z :=
     fold_right Z.add 0%Z (map (fun t => fst t * snd t) p).
-  
+
   Lemma eval_nil : eval nil = 0.
   Proof. trivial.                                             Qed.
   Lemma eval_cons p q : eval (p::q) = fst p * snd p + eval q.
@@ -24,7 +24,7 @@ Module Associational.
   Lemma eval_app p q: eval (p++q) = eval p + eval q.
   Proof. induction p; rewrite <-?List.app_comm_cons;
            rewrite ?eval_nil, ?eval_cons; nsatz.              Qed.
-  
+
   Hint Rewrite eval_nil eval_cons eval_app : push_eval.
   Local Ltac push := autorewrite with
       push_eval push_map push_partition push_flat_map
@@ -190,7 +190,7 @@ Example base_25_5_mul (f g:tuple Z 10) :
   cbv -[runtime_mul runtime_add]; cbv [runtime_mul runtime_add].
   ring_simplify_subterms.
 (* ?fg =
- (f0*g9+ f1*g8+    f2*g7+    f3*g6+    f4*g5+    f5*g4+    f6*g3+    f7*g2+    f8*g1+    f9*g0,   
+ (f0*g9+ f1*g8+    f2*g7+    f3*g6+    f4*g5+    f5*g4+    f6*g3+    f7*g2+    f8*g1+    f9*g0,
   f0*g8+ 2*f1*g7+  f2*g6+    2*f3*g5+  f4*g4+    2*f5*g3+  f6*g2+    2*f7*g1+  f8*g0+    38*f9*g9,
   f0*g7+ f1*g6+    f2*g5+    f3*g4+    f4*g3+    f5*g2+    f6*g1+    f7*g0+    19*f8*g9+ 19*f9*g8,
   f0*g6+ 2*f1*g5+  f2*g4+    2*f3*g3+  f4*g2+    2*f5*g1+  f6*g0+    38*f7*g9+ 19*f8*g8+ 38*f9*g7,
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index 71100cdcf..b3148efdb 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -3,8 +3,9 @@ Require Import Coq.Lists.List. Import ListNotations.
 Require Import Crypto.Arithmetic.Core. Import B.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Arithmetic.Saturated.Freeze.
-Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable.
-Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Require Crypto.Util.Tuple.
 Require Import Crypto.Util.QUtil.
 Local Notation tuple := Tuple.tuple.
diff --git a/src/Specific/ArithmeticSynthesisTest130.v b/src/Specific/ArithmeticSynthesisTest130.v
index 15485499b..e9e40df19 100644
--- a/src/Specific/ArithmeticSynthesisTest130.v
+++ b/src/Specific/ArithmeticSynthesisTest130.v
@@ -2,8 +2,9 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
 Require Import Coq.Lists.List. Import ListNotations.
 Require Import Crypto.Arithmetic.Core. Import B.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable.
-Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Require Crypto.Util.Tuple.
 Local Notation tuple := Tuple.tuple.
 Local Open Scope list_scope.
diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v
index 7d329a613..eaefd0493 100644
--- a/src/Specific/Karatsuba.v
+++ b/src/Specific/Karatsuba.v
@@ -4,12 +4,13 @@ Require Import Crypto.Arithmetic.Core. Import B.
 Require Import Crypto.Arithmetic.Saturated.Core.
 Require Import Crypto.Arithmetic.Saturated.Freeze.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable.
-Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
 Require Import Crypto.Arithmetic.Karatsuba.
 Require Crypto.Util.Tuple.
 Require Import Crypto.Util.IdfunWithAlt.
 Require Import Crypto.Util.QUtil.
+Require Import Crypto.Util.Tactics.VM.
 Local Notation tuple := Tuple.tuple.
 Local Open Scope list_scope.
 Local Open Scope Z_scope.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index e99197ece..d85ab027b 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -3,7 +3,7 @@ Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil.
 Require Import Coqprime.Zp.
 Require Export Crypto.Util.FixCoqMistakes.
-Require Export Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Local Open Scope Z.
 
 (* TODO: move somewhere else for lemmas about Coqprime? *)
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v
index 18822cbe3..e8897431a 100644
--- a/src/Util/ZUtil/AddGetCarry.v
+++ b/src/Util/ZUtil/AddGetCarry.v
@@ -2,10 +2,11 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.Hints.ZArith.
-Require Import Crypto.Util.Prod Crypto.Util.Tactics.
+Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Local Open Scope Z_scope.
 
 Local Notation eta x := (fst x, snd x).
@@ -62,7 +63,7 @@ Module Z.
         Z.add_get_carry Z.add_with_get_carry Z.add_with_carry
         Z.sub_get_borrow_full Z.sub_with_get_borrow_full
         Z.sub_get_borrow Z.sub_with_get_borrow Z.sub_with_borrow.
-  
+
   Lemma add_get_carry_full_mod s x y :
     fst (Z.add_get_carry_full s x y)  = (x + y) mod s.
   Proof. easypeasy. Qed.