diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-30 14:23:43 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-30 14:23:43 -0400 |
commit | 1b9f8c10fef9b8cff935deda8e89b8351703b119 (patch) | |
tree | 797cebc62ca59d259bade2306aad1aabf8cf3531 /src/Specific/GF25519Reflective/Reified/Sub.v | |
parent | 94793ff420b2d0af6da59eba882e5614abe7e3e3 (diff) |
Add reification of various operations
We split the reification up into separate files, one operation per file,
so that we can run all the reification in parallel when building.
Diffstat (limited to 'src/Specific/GF25519Reflective/Reified/Sub.v')
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Sub.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v new file mode 100644 index 000000000..2695da171 --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/Sub.v @@ -0,0 +1,3 @@ +Require Import Crypto.Specific.GF25519Reflective.Common. + +Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined. |