diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-07-08 16:17:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-07-08 16:17:02 -0400 |
| commit | 59dec7e5b97b447e91a8d86440848f4c5d74c93f (patch) | |
| tree | f577b6f4b71c1f426823e9257af3c0db94b29a80 /src/Specific/ArithmeticSynthesisTest130.v | |
| parent | 86772a8a67e246ba93c708bdb0459f2f39edb966 (diff) | |
More fine-grained tactics imports
Diffstat (limited to 'src/Specific/ArithmeticSynthesisTest130.v')
| -rw-r--r-- | src/Specific/ArithmeticSynthesisTest130.v | 5 |
1 files changed, 3 insertions, 2 deletions
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. |