diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-05 22:32:49 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
| commit | ffa0731cc244091460586b46bf4817e5a918ba49 (patch) | |
| tree | 05bfc8058a8af3469d3652d8a7b95ca5ab45c37f /src/Specific/X25519/C64 | |
| parent | b6e37eee58b0a8f43711533d49392172786e2cb5 (diff) | |
Reorgainze synthesis framework files into a Framework folder
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. |