diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-16 17:02:30 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-06-16 19:41:10 -0400 |
| commit | bf86eb3bb543191bb75784767f39c6d2253c5bac (patch) | |
| tree | 95e4603c1a1f2804910285c16fb24b016941e976 /_CoqProject | |
| parent | c2cfdbede87ffb0489384fe41365961fbd4d1df8 (diff) | |
Switch to using tuples for word-by-word montgomery
The new parameterized definitions and proofs are in
WordByWord/Abstract/Dependent/*; the old ones are untouched (and unused)
in WordByWord/Abstract/*. I replaced definitions I didn't know how to
write in the Saturated API with the use of an axiom.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index e2724bd12..eec30c5b3 100644 --- a/_CoqProject +++ b/_CoqProject @@ -27,6 +27,8 @@ src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v +src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition.v +src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v src/Compilers/CommonSubexpressionElimination.v src/Compilers/CommonSubexpressionEliminationDenote.v src/Compilers/CommonSubexpressionEliminationInterp.v |