From 5a2bb6ac51fe7db51e06bd5d74d21541bb43a2da Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 11 Nov 2018 01:55:20 -0500 Subject: parenthesize proofs in Weierstrass.Projective (closes #456) --- src/Curves/Weierstrass/Projective.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/Curves') 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. -- cgit v1.2.3