diff options
Diffstat (limited to 'src/Assembly/GF25519.v')
| -rw-r--r-- | src/Assembly/GF25519.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 2e6329f18..9a9215c4d 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -205,6 +205,11 @@ Module GF25519. Module Opp := Pipeline OppExpr. End GF25519. +Set Printing All. +Opaque eadd esub emul eshiftr eand toT fromT. +Eval cbv iota beta delta in GF25519.Add.HL.progZ. +Eval cbv iota beta delta in GF25519.Add.AST.progZ. + Extraction "GF25519Add" GF25519.Add. Extraction "GF25519Sub" GF25519.Sub. Extraction "GF25519Mul" GF25519.Mul. |