diff options
Diffstat (limited to 'src/Compilers/Z/InterpSideConditions.v')
| -rw-r--r-- | src/Compilers/Z/InterpSideConditions.v | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/Compilers/Z/InterpSideConditions.v b/src/Compilers/Z/InterpSideConditions.v deleted file mode 100644 index bc3c8f6a9..000000000 --- a/src/Compilers/Z/InterpSideConditions.v +++ /dev/null @@ -1,9 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.InterpSideConditions. -Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Notations. - -Definition InterpSideConditions {t} (e : Expr t) : interp_flat_type interp_base_type (domain t) -> pointed_Prop - := InterpSideConditions interp_op (@interped_op_side_conditions) e. |