diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.txt | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 8 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 10 |
3 files changed, 16 insertions, 6 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 1c4fd2eba4..fd3101613a 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -143,7 +143,9 @@ file list(s): These files are also used by the experimental ocamlbuild plugin, which is quite touchy about them : be careful with order, duplicated entries, whitespace errors, and do not mention .mli there. - - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) + If module B depends on module A, then B should be after A in the .mllib + file. +- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) - The definitions in Makefile.common might have to be adapted too. - If your file needs a specific rule, add it to Makefile.build diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 16a31790a4..ab78b0956f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -49,6 +49,14 @@ We changed the type of the following functions: a functional way. The old style of passing `evar_map`s as references is not supported anymore. +Changes in the abstract syntax tree: + +- The practical totality of the AST has been nodified using + `CAst.t`. This means that all objects coming from parsing will be + indeed wrapped in a `CAst.t`. `Loc.located` is on its way to + deprecation. Some minor interfaces changes have resulted from + this. + We have changed the representation of the following types: - `Lib.object_prefix` is now a record instead of a nested tuple. diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0003a2c217..c48c2d5d16 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -41,15 +41,15 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -local + ./configure -profile devel make clean make -j4 coqide printers -The "-annotate" option is essential when one wants to use Merlin. +The "-profile devel" enables all options recommended for developers (like +warnings, support for Merlin, etc). Moreover Coq is configured so that +it can be run without installing it (i.e. from the current directory). -The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install - -Then check if +Once the compilation is over check if - bin/coqtop - bin/coqide behave as expected. |