Skip to content

Commit 74f668a

Browse files
authored
Update INSTALL.md
1 parent cde1454 commit 74f668a

File tree

1 file changed

+6
-8
lines changed

1 file changed

+6
-8
lines changed

INSTALL.md

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -67,10 +67,10 @@ to have a dedicated `opam` switch (see below).
6767
To get the source code:
6868

6969
# git clone https://github.com/MetaCoq/metacoq.git
70-
# git checkout -b coq-8.14 origin/coq-8.14
70+
# git checkout -b coq-8.16 origin/coq-8.16
7171
# git status
7272

73-
This checks that you are indeed on the `coq-8.14` branch.
73+
This checks that you are indeed on the `coq-8.16` branch.
7474

7575
### Setting up an `opam` switch
7676

@@ -109,14 +109,12 @@ the sources directory.
109109
Then use:
110110

111111
- `make` to compile the `template-coq` plugin, the `pcuic`
112-
development and the `safechecker` and `erasure` plugins.
112+
development and the `safechecker` and `erasure` plugins,
113+
along with the `test-suite`, `translations`, `examples`
114+
and `quotation` libraries.
113115
You can also selectively build each target.
114116

115-
- `make translations` to compile the translation plugins
116-
117-
- `make test-suite` to compile the test suite
118-
119-
- `make install` to install the plugin in `Coq`'s `user-contrib` local
117+
- `make install` to install the plugins in `Coq`'s `user-contrib` local
120118
library. Then the `MetaCoq` namespace can be used for `Require
121119
Import` statements, e.g. `From MetaCoq.Template Require Import All.`.
122120

0 commit comments

Comments
 (0)