diff options
Diffstat (limited to 'src/Specific/Framework/IntegrationTestDisplayCommon.v')
| -rw-r--r-- | src/Specific/Framework/IntegrationTestDisplayCommon.v | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/src/Specific/Framework/IntegrationTestDisplayCommon.v b/src/Specific/Framework/IntegrationTestDisplayCommon.v deleted file mode 100644 index a3bf52d85..000000000 --- a/src/Specific/Framework/IntegrationTestDisplayCommon.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Crypto.Util.Sigma.Lift. -Require Import Crypto.Util.Sigma.Associativity. -Require Import Crypto.Util.Sigma.MapProjections. -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Compilers.Eta. -Require Export Coq.ZArith.ZArith. -Require Export Crypto.Util.LetIn. -Require Export Crypto.Util.FixedWordSizes. -Require Export Crypto.Compilers.Syntax. -Require Export Crypto.Specific.Framework.IntegrationTestDisplayCommonTactics. -Require Export Crypto.Compilers.Z.HexNotationConstants. -Require Export Crypto.Util.Notations. -Require Export Crypto.Compilers.Z.CNotations. - -Global Arguments Pos.to_nat !_ / . -Global Arguments InterpEta {_ _ _ _ _}. -Global Set Printing Width 2000000. - -Notation "'Interp-η' f x" := (Eta.InterpEta f x) (format "'Interp-η' '//' f '//' x", at level 200, f at next level, x at next level). -Notation ReturnType := (interp_flat_type _). -Notation "'let' ( a , b ) := c 'in' d" := (let (a, b) := c in d) (at level 200, d at level 200, format "'let' ( a , b ) := c 'in' '//' d"). - -Require Export Coq.Unicode.Utf8. (* for better line breaks at function display; must come last *) |