From d19c06ae542e49768c63ec9bbffafad4560b9d48 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 26 Jan 2017 10:42:54 +0100
Subject: [PATCH] Typo.

---
 theories/algebra/csum.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 05bdbd340..84181b21c 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -30,12 +30,12 @@ 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'
+  | Cinr_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'
+  | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
 Existing Instance csum_dist.
 
-- 
GitLab