From 634fdbb687e143907004d23f7f6485ae431aaa31 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 Oct 2016 16:17:15 +0200
Subject: [PATCH] Fix typo.

---
 base_logic/primitive.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index a7c13e15f..2850a5921 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -584,7 +584,7 @@ Proof. unseal. by destruct mx. Qed.
 (* Functions *)
 Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
-Lemma cofe_moreC_equivI {A B : cofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma cofe_morC_equivI {A B : cofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 End primitive.
 End uPred_primitive.
-- 
GitLab