diff options
| author | Jasper Hugunin | 2020-08-25 13:02:59 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:32 -0700 |
| commit | e5880b643bb9ce6974d3ecffd8edcbfad9f45cd4 (patch) | |
| tree | 07d1dc847568606af0d8f5687287f0dec819c9bb | |
| parent | d5f04bd6baf88cc24ac29fa955a123e013e14bce (diff) | |
Modify Relations/Relations.v to compile with -mangle-names
| -rw-r--r-- | theories/Relations/Relations.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 0a5128f093..dea76694f3 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -16,16 +16,16 @@ Lemma inverse_image_of_equivalence : forall (A B:Type) (f:A -> B) (r:relation B), equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). Proof. - intros; split; elim H; red; auto. + intros A B f r H; split; elim H; red; auto. intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. Qed. Lemma inverse_image_of_eq : forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y). Proof. - split; red; + intros A B f; split; red; [ (* reflexivity *) reflexivity - | (* transitivity *) intros; transitivity (f y); assumption + | (* transitivity *) intros x y z; transitivity (f y); assumption | (* symmetry *) intros; symmetry ; assumption ]. Qed. |