diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-02 00:01:35 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-06-05 18:47:35 -0400 |
| commit | 7488682db4cf259e0bb0c886e13301c32a2eeaa2 (patch) | |
| tree | 9baf80699c9f00b01d3180504d58351b6ecc0f33 /src/Algebra/Field.v | |
| parent | c4a0d1fdde22dbd2faaa1753e973ee9602076ee8 (diff) | |
Don't rely on autogenerated names
This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).
Diffstat (limited to 'src/Algebra/Field.v')
| -rw-r--r-- | src/Algebra/Field.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index b5b65f161..d46f10190 100644 --- a/src/Algebra/Field.v +++ b/src/Algebra/Field.v @@ -19,7 +19,7 @@ Section Field. Lemma left_inv_unique x ix : ix * x = one -> ix = inv x. Proof using Type*. intro Hix. - assert (ix*x*inv x = inv x). + assert (H0 : ix*x*inv x = inv x). - rewrite Hix, left_identity; reflexivity. - rewrite <-associative, right_multiplicative_inverse, right_identity in H0; trivial. intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix. @@ -39,8 +39,8 @@ Section Field. Lemma mul_cancel_l_iff : forall x y, y <> 0 -> (x * y = y <-> x = one). Proof using Type*. - intros. - split; intros. + intros x y H0. + split; intros H1. + rewrite <-(right_multiplicative_inverse y) by assumption. rewrite <-H1 at 1; rewrite <-associative. rewrite right_multiplicative_inverse by assumption. |