From b8d05916f64136cf809de1fbfd0263a47d192e5e Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Tue, 25 Aug 2020 13:35:24 -0700 Subject: Modify Numbers/NatInt/NZPow.v to compile with -mangle-names --- theories/Numbers/NatInt/NZPow.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 01a15686e0..3b2a496229 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -238,7 +238,7 @@ Qed. Lemma pow_le_mono : forall a b c d, 0 b<=d -> a^b <= c^d. Proof. - intros. transitivity (a^d). + intros a b c d ? ?. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. Qed. -- cgit v1.2.3