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/RewriterAll.v | |
| parent | be2789ada63a1a5a6710da1abc73430f9b676399 (diff) | |
sed s'/RewriterProofs/RewriterAll/g'
Diffstat (limited to 'src/RewriterAll.v')
| -rw-r--r-- | src/RewriterAll.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/RewriterAll.v b/src/RewriterAll.v new file mode 100644 index 000000000..c2a891de1 --- /dev/null +++ b/src/RewriterAll.v @@ -0,0 +1,24 @@ +Require Import Crypto.Rewriter.NBE. +Require Import Crypto.Rewriter.Arith. +Require Import Crypto.Rewriter.ArithWithCasts. +Require Import Crypto.Rewriter.StripLiteralCasts. +Require Import Crypto.Rewriter.ToFancy. +Require Import Crypto.Rewriter.ToFancyWithCasts. + +Module Compilers. + Export NBE.Compilers. + Export Arith.Compilers. + Export ArithWithCasts.Compilers. + Export StripLiteralCasts.Compilers. + Export ToFancy.Compilers. + Export ToFancyWithCasts.Compilers. + + Module Import RewriteRules. + Export NBE.Compilers.RewriteRules. + Export Arith.Compilers.RewriteRules. + Export ArithWithCasts.Compilers.RewriteRules. + Export StripLiteralCasts.Compilers.RewriteRules. + Export ToFancy.Compilers.RewriteRules. + Export ToFancyWithCasts.Compilers.RewriteRules. + End RewriteRules. +End Compilers. |