aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject10
1 files changed, 7 insertions, 3 deletions
diff --git a/_CoqProject b/_CoqProject
index 9f5a239e1..2ca7a4b89 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,12 +35,10 @@ src/MiscCompilerPasses.v
src/MiscCompilerPassesProofs.v
src/PreLanguage.v
src/Rewriter.v
-src/RewriterFull.v
src/RewriterInterpProofs1.v
src/RewriterProofs.v
+src/RewriterProofsTactics.v
src/RewriterRules.v
-src/RewriterRulesGood.v
-src/RewriterRulesInterpGood.v
src/RewriterRulesProofs.v
src/RewriterWf1.v
src/RewriterWf2.v
@@ -121,6 +119,12 @@ src/PushButtonSynthesis/UnsaturatedSolinas.v
src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v
src/PushButtonSynthesis/WordByWordMontgomery.v
src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v
+src/Rewriter/Arith.v
+src/Rewriter/ArithWithCasts.v
+src/Rewriter/NBE.v
+src/Rewriter/StripLiteralCasts.v
+src/Rewriter/ToFancy.v
+src/Rewriter/ToFancyWithCasts.v
src/Spec/CompleteEdwardsCurve.v
src/Spec/Ed25519.v
src/Spec/EdDSA.v