1 files changed, 8 insertions, 6 deletions
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index 2ad567c92..e6305f798 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -11,6 +11,8 @@ Require Import Crypto.Algebra.
 
 Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic.
 
+Require Export Crypto.Util.FixCoqMistakes.
+
 Generalizable All Variables.
 Section PointEncodingPre.
   Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
@@ -22,7 +24,7 @@ Section PointEncodingPre.
   Local Notation "x '^' 2" := (x*x) (at level 30).
 
   Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
-  
+
   Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}.
   Definition F_eqb x y := if eq_dec x y then true else false.
   Lemma F_eqb_iff : forall x y, F_eqb x y = true <-> x == y.
@@ -64,7 +66,7 @@ Section PointEncodingPre.
     symmetry.
     apply E.solve_correct; eassumption.
   Qed.
- 
+
   (* TODO : move? *)
   Lemma square_opp : forall x : F, (opp x ^2) == (x ^2).
   Proof.
@@ -97,7 +99,7 @@ Section PointEncodingPre.
           let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in
           if (andb (F_eqb x 0) (whd w))
           then None (* special case for 0, since its opposite has the same sign; if the sign bit of 0 is 1, produce None.*)
-          else Some p 
+          else Some p
         else None
     end.
 
@@ -112,7 +114,7 @@ Section PointEncodingPre.
     destruct x as [x1 x2].
     destruct y as [y1 y2].
     match goal with
-    | |- {prod_eq _ _ (?x1, ?x2) (?y1,?y2)} + {not (prod_eq _ _ (?x1, ?x2) (?y1,?y2))} => 
+    | |- {prod_eq _ _ (?x1, ?x2) (?y1,?y2)} + {not (prod_eq _ _ (?x1, ?x2) (?y1,?y2))} =>
       destruct (A_eq_dec x1 y1); destruct (A_eq_dec x2 y2) end;
       unfold prod_eq; intuition.
   Qed.
@@ -162,7 +164,7 @@ Section PointEncodingPre.
 
   Definition point_eq (p q : point) : Prop := prod_eq eq eq (proj1_sig p) (proj1_sig q).
   Definition option_point_eq := option_eq (point_eq).
-  
+
   Lemma option_point_eq_iff : forall p q,
     option_point_eq (Some p) (Some q) <->
     option_coordinates_eq (Some (proj1_sig p)) (Some (proj1_sig q)).
@@ -214,7 +216,7 @@ Section PointEncodingPre.
   Proof.
     unfold prod_eq; intros.
     repeat break_let.
-    intuition; etransitivity; eauto.
+    intuition auto with relations; etransitivity; eauto.
   Qed.
 
   Lemma option_coordinates_eq_sym : forall p q, option_coordinates_eq p q ->