diff options
| author | Jasper Hugunin | 2020-08-24 15:52:32 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:31 -0700 |
| commit | 25d1767bd378d555f3cbcda303639d7a4604c759 (patch) | |
| tree | 2bccee8a5a911196dae8be34f3ca746a77188701 | |
| parent | 774d72febd0ddacc57f7b6c60e004796c84ef38b (diff) | |
Modify Classes/CRelationClasses.v to compile with -mangle-names
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index a27919dd43..72a196ca7a 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -319,7 +319,7 @@ Section Binary. split; red; unfold relation_equivalence, iffT. - firstorder. - firstorder. - - intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. + - intros x y z X X0 x0 y0. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. Qed. Global Instance relation_implication_preorder : PreOrder (@subrelation A). @@ -346,7 +346,7 @@ Section Binary. Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). Proof. unfold flip; constructor; unfold flip. - - intros. apply H. apply symmetry. apply X. + - intros X. apply H. apply symmetry. apply X. - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed. End Binary. |