Skip to content

Commit e5ead2c

Browse files
committed
doc: Add missing step to include Rocq repo when building from source
1 parent a789bdb commit e5ead2c

File tree

1 file changed

+7
-2
lines changed

1 file changed

+7
-2
lines changed

INSTALL.md

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,11 +85,16 @@ This creates the `rocq.9.1` switch which initially contains only the
8585
basic `OCaml` `4.14.0` compiler with the `flambda` option enabled,
8686
and puts you in the right environment (check with `ocamlc -v`).
8787

88-
Once in the right switch, you can install `Rocq` and the `Equations` package using:
88+
Once in the right switch, you can install `Rocq` and the `Equations` package.
89+
For that, you need to first add the Rocq packages repository, using:
90+
91+
# opam repo add rocq-released https://rocq-prover.org/opam/release, using:
92+
93+
Then, to install the dependencies, it suffices to do:
8994

9095
# opam install . --deps-only
9196

92-
If the commands are successful you should have `coq` available (check with `coqc -v**).
97+
If the commands are successful you should have `rocq` available (check with `rocq -v**).
9398

9499

95100
**Remark:** You can create a [local switch](https://opam.ocaml.org/blog/opam-20-tips/#Local-switches) for

0 commit comments

Comments
 (0)