diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2018-11-11 01:55:20 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2018-11-11 10:22:54 -0500 |
| commit | 5a2bb6ac51fe7db51e06bd5d74d21541bb43a2da (patch) | |
| tree | 1416fe94f234fdd6fd061418d8c1416635bb2bfa /src/Curves | |
| parent | 15948adcbf406b7d4be156d2024d4717161f0b95 (diff) | |
parenthesize proofs in Weierstrass.Projective (closes #456)
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Weierstrass/Projective.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Curves/Weierstrass/Projective.v b/src/Curves/Weierstrass/Projective.v index dca2a9130..93831f73f 100644 --- 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. |