diff options
| author | Jasper Hugunin | 2021-01-08 14:00:50 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2021-01-08 14:00:50 -0800 |
| commit | e2850002db0271aff914c6a81d17354991b0d5cb (patch) | |
| tree | 6e748be69a94a46f61644b0e65577aff97b0e6fb | |
| parent | d68d5d35e529cf6f7a9ef0e7639c92dd9b58540c (diff) | |
Modify Classes/SetoidClass.v to compile with -mangle-names
| -rw-r--r-- | theories/Classes/SetoidClass.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 6a98af39aa..3e71a60fa6 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -87,7 +87,7 @@ Tactic Notation "clsubst" "*" := clsubst_nofail. Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z. Proof with auto. - intros; intro. + intros A ? x y z H H0 H1. assert(z == y) by (symmetry ; auto). assert(x == y) by (transitivity z ; eauto). contradiction. @@ -95,7 +95,7 @@ Qed. Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. - intros; intro. + intros A ? x y z **; intro. assert(y == x) by (symmetry ; auto). assert(y == z) by (transitivity x ; eauto). contradiction. |