From 9883e152767acdaaa29ba8506695bdd64869f407 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Jan 2019 10:33:56 +0100
Subject: [PATCH] Better use of unicode in type classes test file.
---
tests/typeclasses.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tests/typeclasses.v b/tests/typeclasses.v
index 6e31f529..899518d5 100644
--- a/tests/typeclasses.v
+++ b/tests/typeclasses.v
@@ -9,7 +9,7 @@ From stdpp Require Import prelude.
[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