From 7488682db4cf259e0bb0c886e13301c32a2eeaa2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 2 Jun 2017 00:01:35 -0400 Subject: 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). --- Bedrock/Nomega.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Bedrock/Nomega.v') 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. -- cgit v1.2.3