diff options
Diffstat (limited to 'src/Encoding/ModularWordEncodingTheorems.v')
| -rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 66617ec29..dd36b3266 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -3,9 +3,9 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Bedrock.Word. -Require Import Crypto.Tactics.VerdiTactics Crypto.Util.Tactics. Require Import Crypto.Spec.Encoding. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.FixCoqMistakes. Require Import Crypto.Spec.ModularWordEncoding. |