From 36f74ae42ca2c604d3d45971c6cb3934bb77473a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 28 Jul 2017 16:17:11 +0200
Subject: [PATCH] Typo
---
theories/algebra/ofe.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index bd5f3e386..c32b4af9e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -586,7 +586,7 @@ Section ofe_mor.
intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
(conv_compl n (ofe_mor_chain c y)) /= Hx.
Qed.
- Global Program Instance ofe_more_cofe `{Cofe B} : Cofe ofe_morC :=
+ Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morC :=
{| compl := ofe_mor_compl |}.
Next Obligation.
intros ? n c x; simpl.
--
GitLab