diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-10 16:41:34 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-04-11 11:01:29 -0400 |
commit | 60520cd8d08f63337225c0a2938827e00a2c48a3 (patch) | |
tree | aaf3a2a7b75aabc1dee784c49da868907f4a1b54 /src | |
parent | be2789ada63a1a5a6710da1abc73430f9b676399 (diff) |
sed s'/RewriterProofs/RewriterAll/g'
Diffstat (limited to 'src')
-rw-r--r-- | src/BoundsPipeline.v | 6 | ||||
-rw-r--r-- | src/CompilersTestCases.v | 4 | ||||
-rw-r--r-- | src/Rewriter/Arith.v | 6 | ||||
-rw-r--r-- | src/Rewriter/ArithWithCasts.v | 6 | ||||
-rw-r--r-- | src/Rewriter/NBE.v | 6 | ||||
-rw-r--r-- | src/Rewriter/StripLiteralCasts.v | 6 | ||||
-rw-r--r-- | src/Rewriter/ToFancy.v | 6 | ||||
-rw-r--r-- | src/Rewriter/ToFancyWithCasts.v | 6 | ||||
-rw-r--r-- | src/RewriterAll.v (renamed from src/RewriterProofs.v) | 0 | ||||
-rw-r--r-- | src/RewriterAllTactics.v (renamed from src/RewriterProofsTactics.v) | 0 |
10 files changed, 23 insertions, 23 deletions
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 |