From 25d1767bd378d555f3cbcda303639d7a4604c759 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Mon, 24 Aug 2020 15:52:32 -0700 Subject: Modify Classes/CRelationClasses.v to compile with -mangle-names --- theories/Classes/CRelationClasses.v | 4 ++-- 1 file 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. -- cgit v1.2.3