Revert "Add apply10"

This reverts commit fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b.

Revert "copy_bounds"

This reverts commit 4c395e83de3c0baf7f8639fa2fbe2b62ba509682.

Revert "Add Common10_4Op"

This reverts commit 677733838139ff09d4a2dd9ff82258492a9a5bab.

Revert "Add Expr10_4Op"

This reverts commit 540740e8a423d0ec9d1dddb173f772c441dc0a1a.

Revert "Add i10top_correct_and_bounded"

This reverts commit bc4184ce6086971799630a0419881c8d344811ca.

Revert "Add appify10"

This reverts commit 66b63b406d9c78a0cecbbf89e5baf282231215c5.

1 files changed, 0 insertions, 54 deletions

diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v
index 82c577dfa..20e8c84fd 100644
--- a/src/SpecificGen/GF5211_32BoundedCommon.v
+++ b/src/SpecificGen/GF5211_32BoundedCommon.v
@@ -206,26 +206,6 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe5211_32W_correct | ]); reflexivity.
   Qed.
-
-  Definition appify10 {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe5211_32W) :=
-    app_fe5211_32W x0 (fun x0' =>
-    app_fe5211_32W x1 (fun x1' =>
-    app_fe5211_32W x2 (fun x2' =>
-    app_fe5211_32W x3 (fun x3' =>
-    app_fe5211_32W x4 (fun x4' =>
-    app_fe5211_32W x5 (fun x5' =>
-    app_fe5211_32W x6 (fun x6' =>
-    app_fe5211_32W x7 (fun x7' =>
-    app_fe5211_32W x8 (fun x8' =>
-    app_fe5211_32W x9 (fun x9' =>
-                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
-
-  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
-      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
-  Proof.
-    intros. cbv [appify10].
-    repeat (etransitivity; [ apply app_fe5211_32W_correct | ]); reflexivity.
-  Qed.
 End generic_destructuring.
 
 Definition eta_fe5211_32W_sig (x : fe5211_32W) : { v : fe5211_32W | v = x }.
@@ -426,24 +406,6 @@ Definition curry_9op_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> fe5211_32W
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
-Definition uncurry_10op_fe5211_32W {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T)
-  := Eval cbv (*-[word64]*) in
-      uncurry_unop_fe5211_32W (fun x0 =>
-      uncurry_unop_fe5211_32W (fun x1 =>
-      uncurry_unop_fe5211_32W (fun x2 =>
-      uncurry_unop_fe5211_32W (fun x3 =>
-      uncurry_unop_fe5211_32W (fun x4 =>
-      uncurry_unop_fe5211_32W (fun x5 =>
-      uncurry_unop_fe5211_32W (fun x6 =>
-      uncurry_unop_fe5211_32W (fun x7 =>
-      uncurry_unop_fe5211_32W (fun x8 =>
-      uncurry_unop_fe5211_32W (fun x9 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
-Definition curry_10op_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T
-  := Eval cbv (*-[word64]*) in
-      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
-                => curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
-
 Definition proj1_fe5211_32W (x : fe5211_32) : fe5211_32W
   := Eval app_tuple_map in
       app_fe5211_32 x (HList.mapt (fun _ => (@proj_word _ _))).
@@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op
               = op (fe5211_32WToZ x0) (fe5211_32WToZ x1) (fe5211_32WToZ x2) (fe5211_32WToZ x3) (fe5211_32WToZ x4) (fe5211_32WToZ x5) (fe5211_32WToZ x6) (fe5211_32WToZ x7) (fe5211_32WToZ x8))
              * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
        (only parsing).
-Notation i10top_correct_and_bounded k irop op
-  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
-          is_bounded (fe5211_32WToZ x0) = true
-          -> is_bounded (fe5211_32WToZ x1) = true
-          -> is_bounded (fe5211_32WToZ x2) = true
-          -> is_bounded (fe5211_32WToZ x3) = true
-          -> is_bounded (fe5211_32WToZ x4) = true
-          -> is_bounded (fe5211_32WToZ x5) = true
-          -> is_bounded (fe5211_32WToZ x6) = true
-          -> is_bounded (fe5211_32WToZ x7) = true
-          -> is_bounded (fe5211_32WToZ x8) = true
-          -> is_bounded (fe5211_32WToZ x9) = true
-          -> (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
-              = op (fe5211_32WToZ x0) (fe5211_32WToZ x1) (fe5211_32WToZ x2) (fe5211_32WToZ x3) (fe5211_32WToZ x4) (fe5211_32WToZ x5) (fe5211_32WToZ x6) (fe5211_32WToZ x7) (fe5211_32WToZ x8) (fe5211_32WToZ x9))
-             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type)
-       (only parsing).
 
 Definition prefreeze := GF5211_32.prefreeze.