diff options
| author | Jasper Hugunin | 2020-10-09 20:21:08 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | 2367d5a90e348a12a52f3aaa66f4e504d7109d67 (patch) | |
| tree | 9be3a5eaf2a204d4b1b58c3f0c617e3a91b6ff81 | |
| parent | 32ce4406474bca0b3fa21834fec978786802a907 (diff) | |
Modify micromega/Ztac.v to compile with -mangle-names
| -rw-r--r-- | theories/micromega/Ztac.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/micromega/Ztac.v b/theories/micromega/Ztac.v index 5fb92aba44..a97ea85ceb 100644 --- a/theories/micromega/Ztac.v +++ b/theories/micromega/Ztac.v @@ -26,7 +26,7 @@ Qed. Lemma elim_concl_eq : forall x y, (x < y \/ y < x -> False) -> x = y. Proof. - intros. + intros x y H. destruct (Z_lt_le_dec x y). exfalso. apply H ; auto. destruct (Zle_lt_or_eq y x);auto. @@ -37,7 +37,7 @@ Qed. Lemma elim_concl_le : forall x y, (y < x -> False) -> x <= y. Proof. - intros. + intros x y H. destruct (Z_lt_le_dec y x). exfalso ; auto. auto. @@ -46,7 +46,7 @@ Qed. Lemma elim_concl_lt : forall x y, (y <= x -> False) -> x < y. Proof. - intros. + intros x y H. destruct (Z_lt_le_dec x y). auto. exfalso ; auto. @@ -93,7 +93,7 @@ Qed. Lemma mul_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1*e2. Proof. - intros. + intros e1 e2 H H0. change 0 with (0* e2). apply Zmult_le_compat_r; auto. Qed. |