From c5f76701ba9c42f8c4ce9881f05904dff677050c Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Thu, 8 Oct 2020 17:15:09 -0700 Subject: Modify Numbers/Integer/Abstract/ZParity.v to compile with -mangle-names --- theories/Numbers/Integer/Abstract/ZParity.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 4b61b18479..0f68278cf0 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -19,19 +19,19 @@ Include NZParityProp Z Z ZP. Lemma odd_pred : forall n, odd (P n) = even n. Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. + intros n. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. Qed. Lemma even_pred : forall n, even (P n) = odd n. Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. + intros n. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. Qed. Lemma even_opp : forall n, even (-n) = even n. Proof. assert (H : forall n, Even n -> Even (-n)). intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv. - intros. rewrite eq_iff_eq_true, !even_spec. + intros n. rewrite eq_iff_eq_true, !even_spec. split. rewrite <- (opp_involutive n) at 2. apply H. apply H. Qed. -- cgit v1.2.3