parenthesize proofs in Weierstrass.Projective (closes #456)

mit-plv · Nov 11, 2018 · 93150cf · 93150cf
1 parent 15948ad
commit 93150cf
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/Curves/Weierstrass/Projective.v b/src/Curves/Weierstrass/Projective.v
@@ -212,12 +212,12 @@ Module Projective.
       all: try abstract fsatz.
 
       (* zero + P = P   -- cases for x and y *)
-      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
-      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+      { assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. }
+      { assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. }
 
       (* P  + zero = P   -- cases for x and y *)
-      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
-      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+      { assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. }
+      { assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. }
     Qed.
   End Projective.
 End Projective.