diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 7 | ||||
| -rw-r--r-- | dev/doc/changes.md | 8 |
2 files changed, 8 insertions, 7 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0506216541..8b0bf216e3 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by the make-based system. -If you want to build the standard libraries and plugins you should -call `make -f Makefile.dune voboot`. It is usually enough to do that -once per-session. - More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. @@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and `coqide` in a fast build. In order to use them, do: ``` -$ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` @@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors: ## Dropping from coqtop: -After doing `make -f Makefile.dune voboot`, the following commands should work: +The following commands should work: ``` dune exec -- dev/shim/coqbyte-prelude > Drop. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index eac8d86b0a..9498ab8bbb 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -9,6 +9,13 @@ ### ML API +Proof state and constant declaration: + +- A large consolidation of the API handling interactive and + non-interactive constant has been performed; low-level APIs are no + longer available, and the functionality of the `Proof_global` module + has been merged into `Declare`. + Notations: - Most operators on numerals have moved to file numTok.ml. @@ -68,7 +75,6 @@ Proof state: information related to the constant declaration. Some functions have been renamed from `start_proof` to `start_lemma` - Plugins that require access to the information about currently opened lemmas can add one of the `![proof]` attributes to their `mlg` entry, which will refine the type accordingly. See |