Minor 8.5 changes

2 files changed, 10 insertions, 8 deletions

diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 322db1792..f10e587d6 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -144,7 +144,7 @@ Section Pre.
     (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
       * c=1 and an extra a in front of x^2 *)
 
-    injection H; clear H; intros.
+    injection H; cbv beta iota; clear H; intros.
 
     Ltac t x1 y1 x2 y2 :=
       assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 3348be1d9..2ad3877ac 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -5,6 +5,8 @@ Require Crypto.CompleteEdwardsCurve.Pre.
 Require Import Crypto.Spec.ModularArithmetic.
 Local Open Scope F_scope.
 
+Global Set Asymmetric Patterns.
+
 Class TwistedEdwardsParams := {
   q : BinInt.Z;
   a : F q;
@@ -19,7 +21,7 @@ Class TwistedEdwardsParams := {
 Module E.
   Section TwistedEdwardsCurves.
     Context {prm:TwistedEdwardsParams}.
-  
+
     (* Twisted Edwards curves with complete addition laws. References:
     * <https://eprint.iacr.org/2008/013.pdf>
     * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
@@ -27,20 +29,20 @@ Module E.
     *)
     Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
     Definition point := { P | onCurve P}.
-  
+
     Definition zero : point := exist _ (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q).
-    
+
     Definition add' P1' P2' :=
       let '(x1, y1) := P1' in
       let '(x2, y2) := P2' in
         (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
-  
+
     Definition add (P1 P2 : point) : point :=
       let 'exist P1' pf1 := P1 in
       let 'exist P2' pf2 := P2 in
       exist _ (add' P1' P2')
         (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2).
-  
+
     Fixpoint mul (n:nat) (P : point) : point :=
       match n with
       | O => zero
@@ -48,7 +50,7 @@ Module E.
       end.
   End TwistedEdwardsCurves.
 End E.
-  
+
 Delimit Scope E_scope with E.
 Infix "+" := E.add : E_scope.
-Infix "*" := E.mul : E_scope.
\ No newline at end of file
+Infix "*" := E.mul : E_scope.