diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-hott.sh | 2 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 4 | ||||
| -rw-r--r-- | dev/doc/debugging.txt | 2 |
3 files changed, 6 insertions, 2 deletions
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 693135a4c9..1bf6e9a872 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 57c7a97d58..a48c491d33 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -18,6 +18,10 @@ We changed the type of the following functions: The returned term contains De Bruijn universe variables. - Global.body_of_constant: same as above. +We renamed the following datatypes: + + Pp.std_ppcmds -> Pp.t + ========================================= = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index 79cde48849..3e2b435b3e 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -1,7 +1,7 @@ Debugging from Coq toplevel using Caml trace mechanism ====================================================== - 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) + 1. Launch bytecode version of Coq (coqtop.byte) 2. Access Ocaml toplevel using vernacular command 'Drop.' 3. Install load paths and pretty printers for terms, idents, ... using Ocaml command '#use "base_include";;' (use '#use "include";;' for |