diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index fafa0c0304..da645bc442 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -39,9 +39,10 @@ When preparing a PR here are some general guidelines: - All files should start with - `{-# OPTIONS --cubical --no-import-sorts --safe #-}` + `{-# OPTIONS --safe #-}` - unless there is a good reason for it not to. + unless there is a good reason for it not to. The `--cubical` and + `--no-import-sorts` flags are added in the `cubical.agda-lib` file. - It is much easier for us to review and merge smaller and self-contained PRs. If a PR changes a lot of files all over the