Add Display files and targets

1 files changed, 2 insertions, 17 deletions

diff --git a/src/Specific/IntegrationTestMul.v b/src/Specific/IntegrationTestMul.v
index ec9120246..0cbc3966e 100644
--- a/src/Specific/IntegrationTestMul.v
+++ b/src/Specific/IntegrationTestMul.v
@@ -11,6 +11,8 @@ Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.MoveLetIn.
 Import ListNotations.
 
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
 Section BoundedField25p5.
@@ -39,23 +41,6 @@ Section BoundedField25p5.
   Let phi : feBW -> F m :=
     fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  (** TODO MOVE ME *)
-  (** The [eexists_sig_etransitivity] tactic takes a goal of the form
-      [{ a | f a = b }], and splits it into two goals, [?b' = b] and
-      [{ a | f a = ?b' }], where [?b'] is a fresh evar. *)
-  Definition sig_eq_trans_exist1 {A B} (f : A -> B)
-             (b b' : B)
-             (pf : b' = b)
-             (y : { a : A | f a = b' })
-    : { a : A | f a = b }
-    := let 'exist a p := y in exist _ a (eq_trans p pf).
-  Ltac eexists_sig_etransitivity :=
-    lazymatch goal with
-    | [ |- { a : ?A | @?f a = ?b } ]
-      => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in
-         simple refine (lem _ _)
-    end.
-
   (* TODO : change this to field once field isomorphism happens *)
   Definition mul :
     { mul : feBW -> feBW -> feBW