diff options
| author | Jasper Hugunin | 2020-10-08 18:40:52 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-08 18:40:52 -0700 |
| commit | d5c202a71004f8f4b2ef7f0f8fc398a8ebcf8065 (patch) | |
| tree | 77f31fcc627762537111baa77ee638985823a46c /theories/ZArith | |
| parent | ef711580200fd216e544c37be715a6c8af157342 (diff) | |
Modify ZArith/Zorder.v to compile with -mangle-names
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zorder.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 7e33fe2b4c..949a01860f 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -354,7 +354,7 @@ Qed. Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n. Proof. - induction n; simpl; intros. apply Z.le_refl. easy. + intros n; induction n; simpl; intros. apply Z.le_refl. easy. Qed. Hint Immediate Z.eq_le_incl: zarith. |