diff options
Diffstat (limited to 'src/Specific/X25519/C64')
-rw-r--r-- | src/Specific/X25519/C64/CurveParameters.v | 2 | ||||
-rw-r--r-- | src/Specific/X25519/C64/Synthesis.v | 2 | ||||
-rw-r--r-- | src/Specific/X25519/C64/femulDisplay.v | 2 | ||||
-rw-r--r-- | src/Specific/X25519/C64/fesquareDisplay.v | 2 | ||||
-rw-r--r-- | src/Specific/X25519/C64/ladderstep.v | 2 | ||||
-rw-r--r-- | src/Specific/X25519/C64/ladderstepDisplay.v | 2 |
6 files changed, 6 insertions, 6 deletions
diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 1e15eea24..3b8016e96 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.CurveParameters. +Require Import Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.LetIn. (*** diff --git a/src/Specific/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v index d77bb5cee..3c3bac04d 100644 --- a/src/Specific/X25519/C64/Synthesis.v +++ b/src/Specific/X25519/C64/Synthesis.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.SynthesisFramework. +Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X25519.C64.CurveParameters. Module Import T := MakeSynthesisTactics Curve. diff --git a/src/Specific/X25519/C64/femulDisplay.v b/src/Specific/X25519/C64/femulDisplay.v index 35c557ce5..0e77976ca 100644 --- a/src/Specific/X25519/C64/femulDisplay.v +++ b/src/Specific/X25519/C64/femulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.femul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/X25519/C64/fesquareDisplay.v b/src/Specific/X25519/C64/fesquareDisplay.v index f39710fec..e722863e2 100644 --- a/src/Specific/X25519/C64/fesquareDisplay.v +++ b/src/Specific/X25519/C64/fesquareDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.fesquare. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display square. diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v index 11238e0b2..adb20912e 100644 --- a/src/Specific/X25519/C64/ladderstep.v +++ b/src/Specific/X25519/C64/ladderstep.v @@ -1,6 +1,6 @@ Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.LadderstepSynthesisFramework. +Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. Require Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) diff --git a/src/Specific/X25519/C64/ladderstepDisplay.v b/src/Specific/X25519/C64/ladderstepDisplay.v index 73aab21ab..0716f8ef1 100644 --- a/src/Specific/X25519/C64/ladderstepDisplay.v +++ b/src/Specific/X25519/C64/ladderstepDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.ladderstep. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display xzladderstep. |