diff options
Diffstat (limited to 'src/Compilers/Z/Inline.v')
| -rw-r--r-- | src/Compilers/Z/Inline.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/Compilers/Z/Inline.v b/src/Compilers/Z/Inline.v deleted file mode 100644 index cbe6dbfde..000000000 --- a/src/Compilers/Z/Inline.v +++ /dev/null @@ -1,10 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Inline. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. - -Definition InlineConstAndOpp {t} (e : Expr t) : Expr t - := @InlineConst base_type op (is_const_or_opp) t e. - -Definition InlineConst {t} (e : Expr t) : Expr t - := @InlineConst base_type op (is_const) t e. |