aboutsummaryrefslogtreecommitdiff
path: root/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v')
-rw-r--r--src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
index 3cee63c4e..8379838f6 100644
--- a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
+++ b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
@@ -1,7 +1,7 @@
(** * Push-Button Synthesis of Unsaturated Solinas: Reification Cache *)
Require Import Coq.ZArith.ZArith.
Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.
+Require Import Crypto.Arithmetic.Core.
Require Import Crypto.PushButtonSynthesis.ReificationCache.
Local Open Scope Z_scope.