aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-09 22:13:17 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-09 22:13:17 -0400
commita37a83ae363394df68c90677b0af904ef70dc4b4 (patch)
tree428a274c0edad0d196bb238160ece8811f2a8ba2 /_CoqProject
parent8ac6a73847e49aa89136c28d02ad6fdd0c72a209 (diff)
Make it clear that the combined definition/proof file is a work in progress
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject2
1 files changed, 1 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject
index 518956f8c..2770bc7db 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -22,8 +22,8 @@ src/Arithmetic/BarrettReduction/HAC.v
src/Arithmetic/BarrettReduction/Wikipedia.v
src/Arithmetic/MontgomeryReduction/Definition.v
src/Arithmetic/MontgomeryReduction/Proofs.v
-src/Arithmetic/MontgomeryReduction/WordByWord/Combined.v
src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
+src/Arithmetic/MontgomeryReduction/WordByWord/TemporaryFileCombined.v
src/Compilers/CommonSubexpressionElimination.v
src/Compilers/CommonSubexpressionEliminationDenote.v
src/Compilers/CommonSubexpressionEliminationInterp.v