aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-07-12 07:01:49 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-07-12 07:01:49 -0400
commite9f6531ab4dbd417bea21e2d1880340dd63fd576 (patch)
tree1813d6df7cbc744c4dc1fce29a27e6c6d0d29b51 /src
parent1aeda9842703d2bb4612a424f84ccc8d62b181e3 (diff)
Remove useless dependency
Diffstat (limited to 'src')
-rw-r--r--src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
index ed448c75c..41f7cca7e 100644
--- a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
+++ b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
@@ -3,7 +3,6 @@ Require Import Coq.derive.Derive.
Require Import Coq.Lists.List.
Require Import Crypto.Experiments.NewPipeline.Arithmetic.
Require Import Crypto.Experiments.NewPipeline.Toplevel1.
-Require Import Crypto.Experiments.NewPipeline.Toplevel2.
Require Import Crypto.Experiments.NewPipeline.CStringification.
Require Import Crypto.Util.Notations.