From 49b5dd500afabdc8314500bcd5ffa50f279cdff8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 21 Oct 2018 14:13:01 +0200
Subject: [PATCH] =?UTF-8?q?Use=20unicide=20=E2=88=A7=20and=20=E2=88=83.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
tests/algebra.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tests/algebra.v b/tests/algebra.v
index 0ec719eac..cc94ecc72 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -18,7 +18,7 @@ End tests.
[2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*)
Lemma test_setoid_rewrite :
- exists R, @Reflexive Prop R /\ R = iff.
+ ∃ R, @Reflexive Prop R ∧ R = iff.
Proof.
eexists. split.
- apply _.
--
GitLab