Revert "Eta-expand pairs in Eta.v"

This reverts commit 778c1906711f68bed5760710712bb16eeb9c2365.

It's not particularly useful, I think, and might be counterproductive;
most of the unfolded pair projections in x86 are applied to variables,
not instructions, and some instructions don't have pair projections
directly applied to them.

1 files changed, 10 insertions, 13 deletions

diff --git a/src/BoundedArithmetic/Eta.v b/src/BoundedArithmetic/Eta.v
index bc9b0e940..b48b8cff1 100644
--- a/src/BoundedArithmetic/Eta.v
+++ b/src/BoundedArithmetic/Eta.v
@@ -2,33 +2,30 @@
 (** This is useful for allowing us to refold the projections. *)
 Require Import Crypto.BoundedArithmetic.Interface.
 
-Local Notation eta x := (fst x, snd x).
-Local Notation eta3 x := (fst x, eta (snd x)).
-
 Definition eta_decode {n W} (x : decoder n W) : decoder n W := {| decode := decode |}.
 Section InstructionGallery.
   Context {n W} {Wdecoder : decoder n W}.
   Definition eta_ldi (x : load_immediate W) := {| ldi := ldi |}.
   Definition eta_shrd (x : shift_right_doubleword_immediate W) := {| shrd := shrd |}.
-  Definition eta_shrdf (x : shift_right_doubleword_immediate_with_CF W) := {| shrdf a b c := eta (shrdf a b c) |}.
+  Definition eta_shrdf (x : shift_right_doubleword_immediate_with_CF W) := {| shrdf := shrdf |}.
   Definition eta_shl (x : shift_left_immediate W) := {| shl := shl |}.
-  Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf a b := eta (shlf a b) |}.
+  Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf := shlf |}.
   Definition eta_shr (x : shift_right_immediate W) := {| shr := shr |}.
-  Definition eta_shrf (x : shift_right_immediate_with_CF W) := {| shrf a b := eta (shrf a b) |}.
-  Definition eta_sprl (x : spread_left_immediate W) := {| sprl a b := eta (sprl a b) |}.
+  Definition eta_shrf (x : shift_right_immediate_with_CF W) := {| shrf := shrf |}.
+  Definition eta_sprl (x : spread_left_immediate W) := {| sprl := sprl |}.
   Definition eta_mkl (x : mask_keep_low W) := {| mkl := mkl |}.
   Definition eta_and (x : bitwise_and W) := {| and := and |}.
-  Definition eta_andf (x : bitwise_and_with_CF W) := {| andf a b := eta (andf a b) |}.
+  Definition eta_andf (x : bitwise_and_with_CF W) := {| andf := andf |}.
   Definition eta_or (x : bitwise_or W) := {| or := or |}.
-  Definition eta_orf (x : bitwise_or_with_CF W) := {| orf a b := eta (orf a b) |}.
-  Definition eta_adc (x : add_with_carry W) := {| adc a b c := eta (adc a b c) |}.
-  Definition eta_subc (x : sub_with_carry W) := {| subc a b c := eta (subc a b c) |}.
+  Definition eta_orf (x : bitwise_or_with_CF W) := {| orf := orf |}.
+  Definition eta_adc (x : add_with_carry W) := {| adc := adc |}.
+  Definition eta_subc (x : sub_with_carry W) := {| subc := subc |}.
   Definition eta_mul (x : multiply W) := {| mul := mul |}.
   Definition eta_mulhwll (x : multiply_low_low W) := {| mulhwll := mulhwll |}.
   Definition eta_mulhwhl (x : multiply_high_low W) := {| mulhwhl := mulhwhl |}.
   Definition eta_mulhwhh (x : multiply_high_high W) := {| mulhwhh := mulhwhh |}.
-  Definition eta_muldw (x : multiply_double W) := {| muldw a b := eta (muldw a b) |}.
-  Definition eta_muldwf (x : multiply_double_with_CF W) := {| muldwf a b := eta3 (muldwf a b) |}.
+  Definition eta_muldw (x : multiply_double W) := {| muldw := muldw |}.
+  Definition eta_muldwf (x : multiply_double_with_CF W) := {| muldwf := muldwf |}.
   Definition eta_selc (x : select_conditional W) := {| selc := selc |}.
   Definition eta_addm (x : add_modulo W) := {| addm := addm |}.
 End InstructionGallery.