diff options
| author | Jasper Hugunin | 2020-08-25 13:35:24 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:33 -0700 |
| commit | b8d05916f64136cf809de1fbfd0263a47d192e5e (patch) | |
| tree | 2059cbdf42b884c4f1fc397608d2878befd062d2 /theories/Numbers | |
| parent | e950f496ba1f8e4662d513a15b4c96e5a3c7ab39 (diff) | |
Modify Numbers/NatInt/NZPow.v to compile with -mangle-names
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 2 |
1 files changed, 1 insertions, 1 deletions
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<a<=c -> 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. |