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, 27 deletions

diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index 5d3b9c263..a9d6c574f 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -196,26 +196,6 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
-Definition appify10 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe{{{k}}}{{{c}}}_{{{w}}}) :=
-  app_n x0 (fun x0' =>
-  app_n x1 (fun x1' =>
-  app_n x2 (fun x2' =>
-  app_n x3 (fun x3' =>
-  app_n x4 (fun x4' =>
-  app_n x5 (fun x5' =>
-  app_n x6 (fun x6' =>
-  app_n x7 (fun x7' =>
-  app_n x8 (fun x8' =>
-  app_n 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_n_correct | ]); reflexivity.
-Qed.
-
 Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op.
 Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T
@@ -249,13 +229,6 @@ Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}}
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
-Definition uncurry_10op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
-  := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 10 op.
-Definition curry_10op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
-  := Eval compute in
-      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
-               => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
-
 Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}.
 Proof.