Commit 36f74ae4 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files


parent e1764691
......@@ -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.
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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment