1 files changed, 0 insertions, 63 deletions
diff --git a/src/ModularArithmetic/FField.v b/src/ModularArithmetic/FField.v
deleted file mode 100644
index 4f2b623e0..000000000
--- a/src/ModularArithmetic/FField.v
+++ /dev/null
@@ -1,63 +0,0 @@
-Require Export Crypto.Spec.ModularArithmetic.
-Require Export Coq.setoid_ring.Field.
-
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-
-Local Open Scope F_scope.
-
-Definition OpaqueF := F.
-Definition OpaqueZmodulo := BinInt.Z.modulo.
-Definition Opaqueadd {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @add p.
-Definition Opaquemul {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @mul p.
-Definition Opaquesub {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @sub p.
-Definition Opaquediv {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @div p.
-Definition Opaqueopp {p} : OpaqueF p -> OpaqueF p := @opp p.
-Definition Opaqueinv {p} : OpaqueF p -> OpaqueF p := @inv p.
-Definition OpaqueZToField {p} : BinInt.Z -> OpaqueF p := @ZToField p.
-Definition Opaqueadd_correct {p} : @Opaqueadd p = @add p := eq_refl.
-Definition Opaquesub_correct {p} : @Opaquesub p = @sub p := eq_refl.
-Definition Opaquemul_correct {p} : @Opaquemul p = @mul p := eq_refl.
-Definition Opaquediv_correct {p} : @Opaquediv p = @div p := eq_refl.
-Global Opaque F OpaqueZmodulo Opaqueadd Opaquemul Opaquesub Opaquediv Opaqueopp Opaqueinv OpaqueZToField.
-
-Definition OpaqueFieldTheory p {prime_p} : @field_theory (OpaqueF p) (OpaqueZToField 0%Z) (OpaqueZToField 1%Z) Opaqueadd Opaquemul Opaquesub Opaqueopp Opaquediv Opaqueinv eq := Eval hnf in @Ffield_theory p prime_p.
-
-Ltac FIELD_SIMPL_idtac FLD lH rl :=
-  let Simpl := idtac (* (protect_fv "field") *) in
-  let lemma := get_SimplifyEqLemma FLD in
-  get_FldPre FLD ();
-  Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
-  get_FldPost FLD ().
-Ltac field_simplify_eq_idtac := let G := Get_goal in field_lookup (PackField FIELD_SIMPL_idtac) [] G.
-
-Ltac F_to_Opaque :=
-  change F with OpaqueF in *;
-  change BinInt.Z.modulo with OpaqueZmodulo in *;
-  change @add with @Opaqueadd in *;
-  change @mul with @Opaquemul in *;
-  change @sub with @Opaquesub in *;
-  change @div with @Opaquediv in *;
-  change @opp with @Opaqueopp in *;
-  change @inv with @Opaqueinv in *;
-  change @ZToField with @OpaqueZToField in *.
-
-Ltac F_from_Opaque p :=
-  change OpaqueF with F in *;
-  change (@sig BinNums.Z (fun z : BinNums.Z => @eq BinNums.Z z (BinInt.Z.modulo z p))) with (F p) in *;
-  change OpaqueZmodulo with BinInt.Z.modulo in *;
-  change @Opaqueopp with @opp in *;
-  change @Opaqueinv with @inv in *;
-  change @OpaqueZToField with @ZToField in *;
-  rewrite ?@Opaqueadd_correct, ?@Opaquesub_correct, ?@Opaquemul_correct, ?@Opaquediv_correct in *.
-
-Ltac F_field_simplify_eq :=
-  lazymatch goal with |- @eq (F ?p) _ _ =>
-    F_to_Opaque;
-    field_simplify_eq_idtac;
-    compute;
-    F_from_Opaque p
-  end.
-
-Ltac F_field := F_field_simplify_eq; [ring|..].
-
-Ltac notConstant t := constr:NotConstant.