Skip to content

Commit 23f9646

Browse files
committed
one tiny extra change
1 parent 627f93b commit 23f9646

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

Modules/Signatures/SignatureCoproduct.v

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,9 +31,6 @@ Section Coprod.
3131
Context {O : UU}.
3232
Context {cpC : Coproducts O C}.
3333

34-
Local Notation hsC := (homset_property C).
35-
36-
3734
Local Notation Signature := (signature C).
3835
Local Notation MOD R := (category_LModule R C).
3936

0 commit comments

Comments
 (0)