fix CONTRIBUTING.md (Deducteam#1039)

* fix CONTRIBUTING.md * update CHANGES
fblanqui · Jan 30, 2024 · f227530 · f227530
1 parent 946ce1d
commit f227530
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -5,7 +5,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ## [Unreleased]
 
-- Add the command `opaque` that opacifies a symbol already defined.
+### Added
+
+- Add the `opaque` command to turn a defined symbol into a constant
+
+### Fixed
+
+- Coq export: do not rename module names
+- Sequential symbols: fix order of rules
 
 ## 2.4.1 (2023-11-22)
 

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -79,10 +79,11 @@ following files:
 - `editors/vscode/lp.configuration.json` (comments configuration),
 - `editors/vscode/syntaxes/lp.tmLanguage.json` (syntax highlighting),
 - `tools/listings.tex`
-- `doc/Makefile`
+- `doc/Makefile.bnf`
 - the User Manual files in the `doc/` repository
 
-and do `make doc` for generating BNF grammars.
+and do `make bnf` to generate the BNF grammar,
+and `make doc` to generate the Sphynx documentation.
 
 **Note:** the `lambdapi.opam` file is generated by dune using the `dune-project`
 file, it _should not be edited manually_. It is still versioned because opam