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 /Bedrock/Nomega.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 'Bedrock/Nomega.v')
| -rw-r--r-- | Bedrock/Nomega.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Bedrock/Nomega.v b/Bedrock/Nomega.v index 5f39f832f..9c550b512 100644 --- a/Bedrock/Nomega.v +++ b/Bedrock/Nomega.v @@ -27,12 +27,12 @@ Theorem Nneq_out : forall n m, n <> m -> nat_of_N n <> nat_of_N m. intuition. - apply nat_of_N_eq in H0; tauto. + match goal with H0 : _ |- _ => apply nat_of_N_eq in H0; tauto end. Qed. Theorem Nlt_out : forall n m, n < m -> (nat_of_N n < nat_of_N m)%nat. - unfold Nlt; intros. + unfold Nlt; intros ?? H. rewrite nat_of_Ncompare in H. apply nat_compare_Lt_lt; assumption. Qed. @@ -46,7 +46,7 @@ Qed. Theorem Nge_out : forall n m, n >= m -> (nat_of_N n >= nat_of_N m)%nat. - unfold Nge; intros. + unfold Nge; intros ?? H. rewrite nat_of_Ncompare in H. apply nat_compare_ge; assumption. Qed. |