diff options
| author |  jadep <jadep@mit.edu> | 2019-03-14 14:53:38 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
| commit | 9c5a967ababd80425fe3b09f17f502ed5f0d6a11 (patch) | |
| tree | b5d491f6406311b0aa3af229015d02d9fc39e384 /_CoqProject | |
| parent | 71820cce3ba80acf0a09d7506c49ba2dd6e32d95 (diff) | |
update _CoqProject, fix indentations, and prune dependencies of new Arithmetic files
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index cc94c6619..33f7d57a2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -20,7 +20,6 @@ src/AbstractInterpretation.v src/AbstractInterpretationProofs.v src/AbstractInterpretationWf.v src/AbstractInterpretationZRangeProofs.v -src/Arithmetic.v src/BoundsPipeline.v src/CLI.v src/COperationSpecifications.v @@ -59,9 +58,20 @@ src/Algebra/Nsatz.v src/Algebra/Ring.v src/Algebra/ScalarMult.v src/Algebra/SubsetoidRing.v +src/Arithmetic/BarrettReduction.v +src/Arithmetic/BaseConversion.v +src/Arithmetic/Core.v +src/Arithmetic/FancyMontgomeryReduction.v +src/Arithmetic/Freeze.v +src/Arithmetic/ModOps.v src/Arithmetic/ModularArithmeticPre.v src/Arithmetic/ModularArithmeticTheorems.v +src/Arithmetic/Partition.v src/Arithmetic/PrimeFieldTheorems.v +src/Arithmetic/Primitives.v +src/Arithmetic/Saturated.v +src/Arithmetic/UniformWeight.v +src/Arithmetic/WordByWordMontgomery.v src/Arithmetic/BarrettReduction/Generalized.v src/Arithmetic/BarrettReduction/HAC.v src/Arithmetic/BarrettReduction/RidiculousFish.v |