aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--README.md10
-rw-r--r--_CoqProject4
-rw-r--r--src/BoundsPipeline.v6
-rw-r--r--src/CompilersTestCases.v4
-rw-r--r--src/Rewriter/Arith.v6
-rw-r--r--src/Rewriter/ArithWithCasts.v6
-rw-r--r--src/Rewriter/NBE.v6
-rw-r--r--src/Rewriter/StripLiteralCasts.v6
-rw-r--r--src/Rewriter/ToFancy.v6
-rw-r--r--src/Rewriter/ToFancyWithCasts.v6
-rw-r--r--src/RewriterAll.v (renamed from src/RewriterProofs.v)0
-rw-r--r--src/RewriterAllTactics.v (renamed from src/RewriterProofsTactics.v)0
13 files changed, 31 insertions, 31 deletions
diff --git a/Makefile b/Makefile
index 42556fcf3..17d57cb07 100644
--- a/Makefile
+++ b/Makefile
@@ -51,7 +51,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
src/RewriterWf1.vo \
src/RewriterWf2.vo \
src/RewriterRulesGood.vo \
- src/RewriterProofs.vo
+ src/RewriterAll.vo
NOBIGMEM_UNMADE_VOFILES := \
src/Curves/Weierstrass/AffineProofs.vo \
src/Curves/Weierstrass/Jacobian.vo \
diff --git a/README.md b/README.md
index 57ef3edf1..ae32333c5 100644
--- a/README.md
+++ b/README.md
@@ -204,7 +204,7 @@ Rewriter.v ←──────────────────────
↗ ↖
RewriterWf2.v RewriterInterpProofs1.v
↖ ↗
-RewriterRules.v RewriterProofsTactics.v
+RewriterRules.v RewriterAllTactics.v
↑ ↑
RewriterRulesProofs.v │
↑ │
@@ -218,7 +218,7 @@ RewriterRulesProofs.v │
↑ ↑ │
└───────┬──────────────────┴───────────────────────────────────────────────────────┘
│
- RewriterProofs.v
+ RewriterAll.v
```
- RewriterRules.v: Defines the list of types of the rewrite rules that
@@ -265,7 +265,7 @@ RewriterRulesProofs.v │
rewriter, taking in interp-goodness of rewrite rules as a
hypothesis.
-- RewriterProofsTactics.v: Defines the tactic
+- RewriterAllTactics.v: Defines the tactic
`RewriteRules.Tactic.make_rewriter` (and a similar tactic notation)
which build the entire `VerifiedRewriter`. They take in the
`include_interp` as in Rewriter.v tactics, as well as an hlist of
@@ -274,12 +274,12 @@ RewriterRulesProofs.v │
rewriter from a list of rewrite rules.
- Rewriter/{NBE, Arith, ArithWithCasts, StripLiteralCasts, ToFancy,
- ToFancyWithCasts}.v: Use the tactic from RewriterProofsTactics.v
+ ToFancyWithCasts}.v: Use the tactic from RewriterAllTactics.v
together with the proven list of rewrite rules from
RewriterRulesProofs.v to reify and reduce the corresponding pass and
generate a rewriter.
-- RewriterProofs.v: `Definition`less file that `Export`s the rewriters
+- RewriterAll.v: `Definition`less file that `Export`s the rewriters
defined in `Rewriter/*.v`
diff --git a/_CoqProject b/_CoqProject
index 2ca7a4b89..4d4b652ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,8 +36,8 @@ src/MiscCompilerPassesProofs.v
src/PreLanguage.v
src/Rewriter.v
src/RewriterInterpProofs1.v
-src/RewriterProofs.v
-src/RewriterProofsTactics.v
+src/RewriterAll.v
+src/RewriterAllTactics.v
src/RewriterRules.v
src/RewriterRulesProofs.v
src/RewriterWf1.v
diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v
index f0c161dc2..6c21d7c64 100644
--- a/src/BoundsPipeline.v
+++ b/src/BoundsPipeline.v
@@ -29,7 +29,7 @@ Require Crypto.CStringification.
Require Crypto.LanguageWf.
Require Crypto.UnderLetsProofs.
Require Crypto.MiscCompilerPassesProofs.
-Require Crypto.RewriterProofs.
+Require Crypto.RewriterAll.
Require Crypto.AbstractInterpretationWf.
Require Crypto.AbstractInterpretationProofs.
Require Import Crypto.Util.Notations.
@@ -39,7 +39,7 @@ Import
Crypto.LanguageWf
Crypto.UnderLetsProofs
Crypto.MiscCompilerPassesProofs
- Crypto.RewriterProofs
+ Crypto.RewriterAll
Crypto.AbstractInterpretationWf
Crypto.AbstractInterpretationProofs
Crypto.Language
@@ -53,7 +53,7 @@ Import
LanguageWf.Compilers
UnderLetsProofs.Compilers
MiscCompilerPassesProofs.Compilers
- RewriterProofs.Compilers
+ RewriterAll.Compilers
AbstractInterpretationWf.Compilers
AbstractInterpretationProofs.Compilers
Language.Compilers
diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v
index 2ed149cdd..91fc3af1d 100644
--- a/src/CompilersTestCases.v
+++ b/src/CompilersTestCases.v
@@ -5,7 +5,7 @@ Require Import Crypto.Util.LetIn.
Require Import Crypto.Language.
Require Import Crypto.UnderLets.
Require Import Crypto.AbstractInterpretation.
-Require Import Crypto.RewriterProofs.
+Require Import Crypto.RewriterAll.
Require Import Crypto.MiscCompilerPasses.
Require Import Crypto.CStringification.
Import ListNotations. Local Open Scope Z_scope.
@@ -13,7 +13,7 @@ Import ListNotations. Local Open Scope Z_scope.
Import Language.Compilers.
Import UnderLets.Compilers.
Import AbstractInterpretation.Compilers.
-Import RewriterProofs.Compilers.
+Import RewriterAll.Compilers.
Import MiscCompilerPasses.Compilers.
Import CStringification.Compilers.
Local Coercion Z.of_nat : nat >-> Z.
diff --git a/src/Rewriter/Arith.v b/src/Rewriter/Arith.v
index cae1526d2..7b368cb16 100644
--- a/src/Rewriter/Arith.v
+++ b/src/Rewriter/Arith.v
@@ -1,15 +1,15 @@
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Language.
Require Import Crypto.LanguageWf.
-Require Import Crypto.RewriterProofsTactics.
+Require Import Crypto.RewriterAllTactics.
Require Import Crypto.RewriterRulesProofs.
Module Compilers.
Import Language.Compilers.
Import Language.Compilers.defaults.
Import LanguageWf.Compilers.
- Import RewriterProofsTactics.Compilers.RewriteRules.GoalType.
- Import RewriterProofsTactics.Compilers.RewriteRules.Tactic.
+ Import RewriterAllTactics.Compilers.RewriteRules.GoalType.
+ Import RewriterAllTactics.Compilers.RewriteRules.Tactic.
Module Import RewriteRules.
Section __.
diff --git a/src/Rewriter/ArithWithCasts.v b/src/Rewriter/ArithWithCasts.v
index de17f207e..554457f1d 100644
--- a/src/Rewriter/ArithWithCasts.v
+++ b/src/Rewriter/ArithWithCasts.v
@@ -1,14 +1,14 @@
Require Import Crypto.Language.
Require Import Crypto.LanguageWf.
-Require Import Crypto.RewriterProofsTactics.
+Require Import Crypto.RewriterAllTactics.
Require Import Crypto.RewriterRulesProofs.
Module Compilers.
Import Language.Compilers.
Import Language.Compilers.defaults.
Import LanguageWf.Compilers.
- Import RewriterProofsTactics.Compilers.RewriteRules.GoalType.
- Import RewriterProofsTactics.Compilers.RewriteRules.Tactic.
+ Import RewriterAllTactics.Compilers.RewriteRules.GoalType.
+ Import RewriterAllTactics.Compilers.RewriteRules.Tactic.
Module Import RewriteRules.
Section __.
diff --git a/src/Rewriter/NBE.v b/src/Rewriter/NBE.v
index 64e38a38d..db0670179 100644
--- a/src/Rewriter/NBE.v
+++ b/src/Rewriter/NBE.v
@@ -1,14 +1,14 @@
Require Import Crypto.Language.
Require Import Crypto.LanguageWf.
-Require Import Crypto.RewriterProofsTactics.
+Require Import Crypto.RewriterAllTactics.
Require Import Crypto.RewriterRulesProofs.
Module Compilers.
Import Language.Compilers.
Import Language.Compilers.defaults.
Import LanguageWf.Compilers.
- Import RewriterProofsTactics.Compilers.RewriteRules.GoalType.
- Import RewriterProofsTactics.Compilers.RewriteRules.Tactic.
+ Import RewriterAllTactics.Compilers.RewriteRules.GoalType.
+ Import RewriterAllTactics.Compilers.RewriteRules.Tactic.
Module Import RewriteRules.
Section __.
diff --git a/src/Rewriter/StripLiteralCasts.v b/src/Rewriter/StripLiteralCasts.v
index 0f35dfed6..8c6c1799c 100644
--- a/src/Rewriter/StripLiteralCasts.v
+++ b/src/Rewriter/StripLiteralCasts.v
@@ -1,14 +1,14 @@
Require Import Crypto.Language.
Require Import Crypto.LanguageWf.
-Require Import Crypto.RewriterProofsTactics.
+Require Import Crypto.RewriterAllTactics.
Require Import Crypto.RewriterRulesProofs.
Module Compilers.
Import Language.Compilers.
Import Language.Compilers.defaults.
Import LanguageWf.Compilers.
- Import RewriterProofsTactics.Compilers.RewriteRules.GoalType.
- Import RewriterProofsTactics.Compilers.RewriteRules.Tactic.
+ Import RewriterAllTactics.Compilers.RewriteRules.GoalType.
+ Import RewriterAllTactics.Compilers.RewriteRules.Tactic.
Module Import RewriteRules.
Section __.
diff --git a/src/Rewriter/ToFancy.v b/src/Rewriter/ToFancy.v
index da18848ba..da77e4f21 100644
--- a/src/Rewriter/ToFancy.v
+++ b/src/Rewriter/ToFancy.v
@@ -1,15 +1,15 @@
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Language.
Require Import Crypto.LanguageWf.
-Require Import Crypto.RewriterProofsTactics.
+Require Import Crypto.RewriterAllTactics.
Require Import Crypto.RewriterRulesProofs.
Module Compilers.
Import Language.Compilers.
Import Language.Compilers.defaults.
Import LanguageWf.Compilers.
- Import RewriterProofsTactics.Compilers.RewriteRules.GoalType.
- Import RewriterProofsTactics.Compilers.RewriteRules.Tactic.
+ Import RewriterAllTactics.Compilers.RewriteRules.GoalType.
+ Import RewriterAllTactics.Compilers.RewriteRules.Tactic.
Module Import RewriteRules.
Section __.
diff --git a/src/Rewriter/ToFancyWithCasts.v b/src/Rewriter/ToFancyWithCasts.v
index 714ea071e..b8e268b1c 100644
--- a/src/Rewriter/ToFancyWithCasts.v
+++ b/src/Rewriter/ToFancyWithCasts.v
@@ -2,15 +2,15 @@ Require Import Coq.ZArith.ZArith.
Require Import Crypto.Language.
Require Import Crypto.LanguageWf.
Require Import Crypto.Util.ZRange.
-Require Import Crypto.RewriterProofsTactics.
+Require Import Crypto.RewriterAllTactics.
Require Import Crypto.RewriterRulesProofs.
Module Compilers.
Import Language.Compilers.
Import Language.Compilers.defaults.
Import LanguageWf.Compilers.
- Import RewriterProofsTactics.Compilers.RewriteRules.GoalType.
- Import RewriterProofsTactics.Compilers.RewriteRules.Tactic.
+ Import RewriterAllTactics.Compilers.RewriteRules.GoalType.
+ Import RewriterAllTactics.Compilers.RewriteRules.Tactic.
Module Import RewriteRules.
Section __.
diff --git a/src/RewriterProofs.v b/src/RewriterAll.v
index c2a891de1..c2a891de1 100644
--- a/src/RewriterProofs.v
+++ b/src/RewriterAll.v
diff --git a/src/RewriterProofsTactics.v b/src/RewriterAllTactics.v
index 22fd16cbb..22fd16cbb 100644
--- a/src/RewriterProofsTactics.v
+++ b/src/RewriterAllTactics.v
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-23 22:30:06 +0000