Skip to content

Commit 75031af

Browse files
authored
Update CONTRIBUTING.md
remove outdated info about Everything.agda
1 parent 02c996f commit 75031af

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

CONTRIBUTING.md

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -103,10 +103,6 @@ When preparing a PR here are some general guidelines:
103103
as well as various versions of function extensionality in
104104
[FunExtEquiv.agda](https://github.com/agda/cubical/blob/master/Cubical/Functions/FunExtEquiv.agda).
105105

106-
- Unless a file is in the `Core`, `Foundations` or `Codata` package you
107-
don't need to add it manually to the `Everything` file as it is
108-
automatically generated when running `make`.
109-
110106
- For folders with `Base` and `Properties` submodules, the `Base` file
111107
can contain some basic consequences of the main definition, but
112108
shouldn't include theorems that would require additional imports.

0 commit comments

Comments
 (0)