6 files changed, 19 insertions, 15 deletions
diff --git a/dev/base_include b/dev/base_include
index bfbf6bb5d8..79ecd73e0d 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -194,8 +194,8 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
+let parse_tac    = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 6560305433..4b3b44875f 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -85,8 +85,8 @@
 ########################################################################
 # fiat_parsers
 ########################################################################
-: ${fiat_parsers_CI_BRANCH:=trunk__API}
-: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git}
+: ${fiat_parsers_CI_BRANCH:=master}
+: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
 
 ########################################################################
 # fiat_crypto
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/build-system.dev.txt b/dev/doc/build-system.dev.txt
index fefcb0937a..f3fc13e969 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -74,25 +74,25 @@ The Makefile is separated in several files :
 - Makefile.doc : specific rules for compiling the documentation.
 
 
-FIND_VCS_CLAUSE
+FIND_SKIP_DIRS
 ---------------
 
-The recommended style of using FIND_VCS_CLAUSE is for example
+The recommended style of using FIND_SKIP_DIRS is for example
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print
 
 1)
 The parentheses even in the one-criteria case is so that if one adds
 other conditions, e.g. change the first example to the second
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
 
 one is not tempted to write
 
- find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print
+ find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print
 
-because this will not necessarily work as expected; $(FIND_VCS_CLAUSE)
+because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
 ends with an -or, and how it combines with what comes later depends on
 operator precedence and all that. Much safer to override it with
 parentheses.
@@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why.
 You are used to write:
  find . -name '*.example'
 and it works fine. But the following will not:
- find . $(FIND_VCS_CLAUSE) -name '*.example'
-it will also list things directly matched by FIND_VCS_CLAUSE
+ find . $(FIND_SKIP_DIRS) -name '*.example'
+it will also list things directly matched by FIND_SKIP_DIRS
 (directories we want to prune, in which we don't want to find
 anything). C'est subtil... Il y a effectivement un -print implicite à
 la fin, qui fait que la commande habituelle sans print fonctionne
 bien, mais dès que l'on introduit d'autres commandes dans le lot (le
--prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de
+-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de
 parenthèses du -print implicite par rapport au parenthésage dans la
 forme recommandée d'utilisation:
 
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