From c885513d41ba5bb2c39f17d7c26f12ea0291f79c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Jun 2016 15:55:30 +0200
Subject: [PATCH] Replace some non-unicode arrows.

---
 algebra/csum.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/algebra/csum.v b/algebra/csum.v
index 9bc08217b..5810079fd 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -8,8 +8,8 @@ Local Arguments cmra_validN _ _ !_ /.
 Local Arguments cmra_valid _  !_ /.
 
 Inductive csum (A B : Type) :=
-| Cinl : A -> csum A B
-| Cinr : B -> csum A B
+| Cinl : A → csum A B
+| Cinr : B → csum A B
 | CsumBot : csum A B.
 Arguments Cinl {_ _} _.
 Arguments Cinr {_ _} _.
@@ -22,13 +22,13 @@ Implicit Types b : B.
 
 (* Cofe *)
 Inductive csum_equiv : Equiv (csum A B) :=
-  | Cinl_equiv a a' : a ≡ a' -> Cinl a ≡ Cinl a'
-  | Cinlr_equiv b b' : b ≡ b' -> Cinr b ≡ Cinr b'
+  | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
+  | Cinlr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
   | CsumBot_equiv : CsumBot ≡ CsumBot.
 Existing Instance csum_equiv.
 Inductive csum_dist : Dist (csum A B) :=
-  | Cinl_dist n a a' : a ≡{n}≡ a' -> Cinl a ≡{n}≡ Cinl a'
-  | Cinlr_dist n b b' : b ≡{n}≡ b' -> Cinr b ≡{n}≡ Cinr b'
+  | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
+  | Cinlr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
 Existing Instance csum_dist.
 
-- 
GitLab