From 4ad619de6befb6a402a9bacf9dd4618a5e76da42 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 7 Aug 2017 10:21:53 +0200
Subject: [PATCH] cofe -> ofe

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

diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index cca9ddba1..ce9ac390d 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -588,9 +588,9 @@ Proof.
 Qed.
 
 (* Functions *)
-Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
-Lemma cofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 
 (* Sig ofes *)
-- 
GitLab