Merge branch 'trunk' into pr379

29 files changed, 574 insertions, 254 deletions

diff --git a/dev/Makefile.oug b/dev/Makefile.oug
deleted file mode 100644
index ee69ea80d..000000000
--- a/dev/Makefile.oug
+++ /dev/null
@@ -1,74 +0,0 @@
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
-
-
-#### Source Code Analysis via Oug ####
-#### Cf http://home.gna.org/oug ####
-
-
-# To be used from top dir : make -f dev/Makefile.oug ...
-
-include Makefile.build
-
-# Oug location: in the path by default, native version
-
-OUG:=oug.x
-
-# NB: coq should have been compiled with the same ocaml version as oug
-
-# NOTA: it seems we obtain more useless elements reported when _not_
-# providing the .mli files, and also when giving a precise start point.
-# TO BE INVESTIGATED
-
-ml_of_cma = $(patsubst %.cmo,%.ml,$(filter %.cmo,$(shell cat $(1:.cma=.mllib.d))))
-local_ml_of_cma = $(filter $(dir $(1))%,$(call ml_of_cma,$(1)))
-mli_of_ml = $(foreach ml,$(1),$(wildcard $(ml)i))
-
-# Analysis of coqtop, without plugins
-
-COREML:=config/coq_config.ml $(call ml_of_cma, $(CORECMA))
-COREMLI:=$(call mli_of_ml,$(COREML))
-
-core.oug:
-	$(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML)
-
-core.useless: core.oug
-	$(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@
-
-core_intf.oug:
-	$(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) $(COREMLI)
-
-core_intf.useless: core_intf.oug
-	$(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@
-
-# Analysis of coqchk, considering only files in the checker/ subdir
-
-CHECKERML:=$(call local_ml_of_cma,checker/check.cma)
-CHECKERMLI:=$(call mli_of_ml,$(CHECKERML))
-
-## BUG: in oug, include dirs have reversed priority compared with ocaml, cannot use CHKLIBS
-MYCHKINCL:=$(MLINCLUDES) -I checker
-
-checker.oug:
-	$(OUG) --dump-data $@ -rectypes $(MYCHKINCL) $(CHECKERML) #$(CHECKERMLI)
-
-checker.useless: checker.oug
-	$(OUG) --load-data $< --no-reduce --print-loc --roots "<Checker.start>" --useless-elements $@
-
-# Analysis of extraction
-
-EXTRACTIONML:=$(call local_ml_of_cma,$(EXTRACTIONCMA))
-EXTRACTIONMLI:=$(call mli_of_ml,$(EXTRACTIONMLI))
-
-extraction.oug:
-	$(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(EXTRACTIONML) #$(EXTRACTIONMLI)
-
-extraction.useless: extraction.oug
-	$(OUG) --load-data $< --no-reduce --print-loc --useless-elements $@
-
-# More to come ...
\ No newline at end of file
diff --git a/dev/base_include b/dev/base_include
index 0abcefc38..242405ae2 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,7 +17,7 @@
 #directory "grammar";;
 #directory "intf";;
 #directory "stm";;
-#directory "ltac";;
+#directory "vernac";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
@@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Pltac.tactic;;
+let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
new file mode 100644
index 000000000..336ce9d8f
--- /dev/null
+++ b/dev/ci/ci-basic-overlay.sh
@@ -0,0 +1,112 @@
+#!/usr/bin/env bash
+
+# This is the basic overlay set for repositories in the CI.
+
+# Maybe we should just use Ruby to have real objects...
+
+########################################################################
+# MathComp
+########################################################################
+: ${mathcomp_CI_BRANCH:=master}
+: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}
+
+########################################################################
+# UniMath
+########################################################################
+: ${UniMath_CI_BRANCH:=master}
+: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
+
+########################################################################
+# Unicoq + Metacoq
+########################################################################
+: ${unicoq_CI_BRANCH:=master}
+: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}
+
+: ${metacoq_CI_BRANCH:=master}
+: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}
+
+########################################################################
+# Mathclasses + Corn
+########################################################################
+: ${math_classes_CI_BRANCH:=v8.6}
+: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+
+: ${Corn_CI_BRANCH:=v8.6}
+: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+
+########################################################################
+# Iris
+########################################################################
+: ${stdpp_CI_BRANCH:=master}
+: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}
+
+: ${Iris_CI_BRANCH:=master}
+: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}
+
+########################################################################
+# HoTT
+########################################################################
+# Temporal overlay
+: ${HoTT_CI_BRANCH:=mz-8.7}
+: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
+# : ${HoTT_CI_BRANCH:=master}
+# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
+
+########################################################################
+# GeoCoq
+########################################################################
+: ${GeoCoq_CI_BRANCH:=master}
+: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}
+
+########################################################################
+# Flocq
+########################################################################
+: ${Flocq_CI_BRANCH:=master}
+: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}
+
+########################################################################
+# Coquelicot
+########################################################################
+: ${Coquelicot_CI_BRANCH:=master}
+: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}
+
+########################################################################
+# CompCert
+########################################################################
+: ${CompCert_CI_BRANCH:=master}
+: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+
+########################################################################
+# VST
+########################################################################
+: ${VST_CI_BRANCH:=master}
+: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+
+########################################################################
+# fiat_parsers
+########################################################################
+: ${fiat_parsers_CI_BRANCH:=master}
+: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+
+########################################################################
+# fiat_crypto
+########################################################################
+: ${fiat_crypto_CI_BRANCH:=master}
+: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+
+########################################################################
+# CoLoR
+########################################################################
+: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color}
+
+########################################################################
+# SF
+########################################################################
+: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz}
+
+########################################################################
+# TLC
+########################################################################
+: ${tlc_CI_BRANCH:=master}
+: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 78ae7f02f..3f0716511 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -1,8 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color
+Color_CI_DIR=${CI_BUILD_DIR}/color
 
-( cd color && make -j ${NJOBS} )
+svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
+
+( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2a6601e04..2711b7eca 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -1,6 +1,66 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -xe
 
+# Coq's tools need an ending slash :S, we should fix them.
+export COQBIN=`pwd`/bin/
 export PATH=`pwd`/bin:$PATH
+
 ls `pwd`/bin
+
+# Where we clone and build external developments
+CI_BUILD_DIR=`pwd`/_build_ci
+
+source ${ci_dir}/ci-user-overlay.sh
+source ${ci_dir}/ci-basic-overlay.sh
+
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+# git_checkout branch url dest will create a git repository
+# in <dest> (if it does not exist already) and checkout the
+# remote branch <branch> from <url>
+git_checkout()
+{
+  local _BRANCH=${1}
+  local _URL=${2}
+  local _DEST=${3}
+
+  # Allow an optional 4th argument for the commit
+  local _COMMIT=${4:-FETCH_HEAD}
+  local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi)
+
+  mkdir -p ${_DEST}
+  ( cd ${_DEST}                                                && \
+    if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \
+    echo "Checking out ${_DEST}"                               && \
+    git fetch ${_URL} ${_BRANCH}                               && \
+    git checkout ${_COMMIT}                                    && \
+    echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+}
+
+checkout_mathcomp()
+{
+  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+}
+
+# this installs just the ssreflect library of math-comp
+install_ssreflect()
+{
+  echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
+
+  checkout_mathcomp ${mathcomp_CI_DIR}
+  ( cd ${mathcomp_CI_DIR}/mathcomp   && \
+    sed -i.bak '/ssrtest/d'     Make && \
+    sed -i.bak '/odd_order/d'   Make && \
+    sed -i.bak '/all\/all.v/d'  Make && \
+    sed -i.bak '/character/d'   Make && \
+    sed -i.bak '/real_closed/d' Make && \
+    sed -i.bak '/solvable/d'    Make && \
+    sed -i.bak '/field/d'       Make && \
+    sed -i.bak '/fingroup/d'    Make && \
+    sed -i.bak '/algebra/d'     Make && \
+    make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+
+  echo -en 'travis_fold:end:ssr.install\\r'
+
+}
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index d4023c916..c78ffdc2c 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -1,10 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
+CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
+
 opam install -j ${NJOBS} -y menhir
-git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
 
 # Patch to avoid the upper version limit
-( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 4a23e51be..40eff03b7 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -1,29 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/math-comp/math-comp.git
+Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
 
-# coquelicot just needs mathcomp
-( cd math-comp/mathcomp && \
-  sed -i.bak '/ssrtest/d'   Make && \
-  sed -i.bak '/odd_order/d'   Make && \
-  sed -i.bak '/all\/all.v/d'  Make && \
-  sed -i.bak '/character/d'   Make && \
-  sed -i.bak '/real_closed/d' Make && \
-  sed -i.bak '/solvable/d'    Make && \
-  sed -i.bak '/field/d'       Make && \
-  sed -i.bak '/fingroup/d'    Make && \
-  sed -i.bak '/algebra/d'     Make && \
-  make -j ${NJOBS} && make install )
+install_ssreflect
 
-# Setup ssr
-# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc
-# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc
+git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR}
 
-# Setup coquelicot
-git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
-
-( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 18d756180..0e791ebbf 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c594f8360..93d39aab0 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -1,12 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git
+fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
 
-( cd fiat-crypto && make -j ${NJOBS} )
-
-# ( cd corn && make -j ${NJOBS} )
+git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
 
+( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
new file mode 100755
index 000000000..c62aa1d85
--- /dev/null
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
+
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
+
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index b9cf649a1..ec19bd993 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -1,9 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
+Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
 
-( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR}
+
+( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 589a826e0..4e5aa2687 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -1,16 +1,16 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-# XXX: replace by generic template
-GeoCoq_CI_BRANCH=master
-GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
+GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
 
-git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL}
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
 
-( cd GeoCoq                                               && \
+( cd ${GeoCoq_CI_DIR}                                     && \
   ./configure.sh                                          && \
   sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
+  sed -i.bak '/Elements\/Book_1\.v/d'                Make && \
+  sed -i.bak '/Elements\/Book_3\.v/d'                Make && \
   coq_makefile -f Make -o Makefile                        && \
   make -j ${NJOBS} )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 8f82ba9f2..1bf6e9a87 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -1,8 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
+HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
-( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
+git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
+
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index e97e2c19e..262dd6fa0 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -1,35 +1,26 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-# XXX: Refactor into install-ssreflect
-git clone --depth 1 https://github.com/math-comp/math-comp.git
-
-# coquelicot just needs mathcomp
-( cd math-comp/mathcomp && \
-  sed -i.bak '/ssrtest/d'     Make && \
-  sed -i.bak '/odd_order/d'   Make && \
-  sed -i.bak '/all\/all.v/d'  Make && \
-  sed -i.bak '/character/d'   Make && \
-  sed -i.bak '/real_closed/d' Make && \
-  sed -i.bak '/solvable/d'    Make && \
-  sed -i.bak '/field/d'       Make && \
-  sed -i.bak '/fingroup/d'    Make && \
-  sed -i.bak '/algebra/d'     Make && \
-  make -j ${NJOBS} && make install )
-
-# Setup ssr = This doesn't work as coq_makefile will pass -q to coqc :S :S
-# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc
-# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc
+stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
+
+Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
+
+install_ssreflect
+
+# Setup Iris first, as it is needed to compute the dependencies
+
+git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
+read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins
 
 # Setup stdpp
-git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
+stdpp_CI_GITURL=${IRIS_DEP[1]}.git
+stdpp_CI_COMMIT=${IRIS_DEP[2]}
 
-( cd coq-stdpp && make -j ${NJOBS} && make install )
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
 
-# Setup Iris
-git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git
+( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
 
-( cd iris-coq && make -j ${NJOBS} )
+# Build iris now
+( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 9127c1895..beb75773b 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -1,12 +1,20 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 1 -b v8.6 https://github.com/math-classes/math-classes.git
-( cd math-classes && make -j ${NJOBS} && make install )
+math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
-git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git
-( cd corn         && make -j ${NJOBS} )
+Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
+# Setup Math-Classes
+
+git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
+
+( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+
+# Setup Corn
+
+git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+
+( cd ${Corn_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index b83379241..bb8188da4 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -1,13 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/math-comp/math-comp.git
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+checkout_mathcomp ${mathcomp_CI_DIR}
 
 # odd_order takes too much time for travis.
-( cd math-comp/mathcomp                              && \
-     sed -i.bak '/PFsection/d'                  Make && \
-     sed -i.bak '/stripped_odd_order_theorem/d' Make && \
-     make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
+( cd ${mathcomp_CI_DIR}/mathcomp                  && \
+  sed -i.bak '/PFsection/d'                  Make && \
+  sed -i.bak '/stripped_odd_order_theorem/d' Make && \
+  make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 9a9bd3648..e31691179 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,16 +1,19 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-# MetaCoq + UniCoq
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
+metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
-git clone --depth 1 https://github.com/unicoq/unicoq.git
+# Setup UniCoq
 
-( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
 
-git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
 
-( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+# Setup MetaCoq
 
+git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
+
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 5e41211f1..7d23ccad9 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -1,9 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz
+# XXX: Needs fixing to properly set the build directory.
+wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
new file mode 100755
index 000000000..700105aed
--- /dev/null
+++ b/dev/ci/ci-template.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Template_CI_BRANCH=master
+Template_CI_GITURL=https://github.com/Template/Template
+Template_CI_DIR=${CI_BUILD_DIR}/Template
+
+git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR}
+
+( cd ${Template_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index 2161a1146..ce2639937 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -1,8 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone https://gforge.inria.fr/git/tlc/tlc.git
+tlc_CI_DIR=${CI_BUILD_DIR}/tlc
 
-( cd tlc && make -j ${NJOBS} )
+git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
+
+( cd ${tlc_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
new file mode 100755
index 000000000..175b82b5f
--- /dev/null
+++ b/dev/ci/ci-unimath.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
+
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
+
+( cd ${UniMath_CI_DIR}                        && \
+  sed -i.bak '/Folds/d'              Makefile && \
+  sed -i.bak '/HomologicalAlgebra/d' Makefile && \
+  make -j ${NJOBS} BUILD_COQ=no )
+
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
new file mode 100644
index 000000000..028574743
--- /dev/null
+++ b/dev/ci/ci-user-overlay.sh
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+
+# Add user overlays here. You can use some logic to detect if you are
+# in your travis branch and conditionally enable the overlay.
+
+# Some useful Travis variables:
+# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables)
+#
+# - TRAVIS_BRANCH: For builds not triggered by a pull request this is
+#   the name of the branch currently being built; whereas for builds
+#   triggered by a pull request this is the name of the branch
+#   targeted by the pull request (in many cases this will be master).
+#
+# - TRAVIS_COMMIT: The commit that the current build is testing.
+#
+# - TRAVIS_PULL_REQUEST: The pull request number if the current job is
+#   a pull request, “false” if it’s not a pull request.
+#
+# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request,
+#   the name of the branch from which the PR originated. "" if the
+#   current job is a push build.
+
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
new file mode 100755
index 000000000..c11195185
--- /dev/null
+++ b/dev/ci/ci-vst.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+VST_CI_DIR=${CI_BUILD_DIR}/VST
+
+# opam install -j ${NJOBS} -y menhir
+git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR}
+
+# Targets are: msl veric floyd
+# Patch to avoid the upper version limit
+( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} )
diff --git a/dev/core.dbg b/dev/core.dbg
index 38b9b2946..f04e5c07b 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -12,7 +12,8 @@ load_printer proofs.cma
 load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
+load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
 load_printer highparsing.cma
-load_printer ltac.cma
+load_printer ltac_plugin.cmo
diff --git a/dev/doc/api.txt b/dev/doc/api.txt
new file mode 100644
index 000000000..5827257b5
--- /dev/null
+++ b/dev/doc/api.txt
@@ -0,0 +1,10 @@
+Recommendations in using the API:
+
+The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
+
+- On type constr, the canonical equality on CIC (up to
+  alpha-conversion and cast removal) is Constr.equal
+- The type constr is abstract, use mkRel, mkSort, etc. to build
+  elements in constr; use "kind_of_term" to analyze the head of a
+  constr; use destRel, destSort, etc. when the head constructor is
+  known
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index f54f3fcc8..03742fb8a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,12 @@
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
 
+* Ocaml *
+
+Coq is compiled with -safe-string enabled and requires plugins to do
+the same. This means that code using `String` in an imperative way
+will fail to compile now. They should switch to `Bytes.t`
+
 * ML API *
 
 We renamed the following functions:
@@ -39,6 +45,26 @@ important things:
   instead
 - Some printing functions were moved from Pptactic to Pputils
 - A part of Tacexpr has been moved to Tactypes
+- The TacFun tactic expression constructor now takes a `Name.t list` for the 
+  variable list rather than an `Id.t option list`.
+
+The folder itself has been turned into a plugin. This does not change much,
+but because it is a packed plugin, it may wreak havoc for third-party plugins
+depending on any module defined in the ltac/ directory. Namely, even if
+everything looks OK at compile time, a plugin can fail to load at link time
+because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with
+an error of the form:
+
+Error: while loading myplugin.cmxs, no implementation available for Foo.
+
+In particular, most EXTEND macros will trigger this problem even if they
+seemingly do not use any Ltac module, as their expansion do.
+
+The solution is simple, and consists in adding a statement "open Ltac_plugin"
+in each file using a Ltac module, before such a module is actually called. An
+alternative solution would be to fully qualify Ltac modules, e.g. turning any
+call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not
+work for EXTEND macros though.
 
 ** Error handling **
 
@@ -50,6 +76,58 @@ important things:
 
 - The header parameter to `user_err` has been made optional.
 
+** Pretty printing **
+
+Some functions have been removed, see pretty printing below for more
+details.
+
+* Pretty Printing and XML protocol *
+
+The type std_cmdpps has been reworked and made the canonical "Coq rich
+document type". This allows for a more uniform handling of printing
+(specially in IDEs). The main consequences are:
+
+ - Richpp has been confined to IDE use. Most of previous uses of the
+   `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API
+   has been updated.
+
+ - The XML protocol will send a new message type of `pp`, which should
+   be rendered client-wise.
+
+ - `Set Printing Width` is deprecated, now width is controlled
+   client-side.
+
+ - `Pp_control` has removed. The new module `Topfmt` implements
+   console control for the toplevel.
+
+ - The impure tag system in Pp has been removed. This also does away
+   with the printer signatures and functors. Now printers tag
+   unconditionally.
+
+ - The following functions have been removed from `Pp`:
+
+   val stras : int * string -> std_ppcmds
+   val tbrk  : int * int -> std_ppcmds
+   val tab   : unit -> std_ppcmds
+   val pifb  : unit -> std_ppcmds
+   val comment  : int -> std_ppcmds
+   val comments : ((int * int) * string) list ref
+   val eval_ppcmds : std_ppcmds -> std_ppcmds
+   val is_empty : std_ppcmds -> bool
+   val t : std_ppcmds -> std_ppcmds
+   val hb : int -> std_ppcmds
+   val vb : int -> std_ppcmds
+   val hvb : int -> std_ppcmds
+   val hovb : int -> std_ppcmds
+   val tb : unit -> std_ppcmds
+   val close : unit -> std_ppcmds
+   val tclose : unit -> std_ppcmds
+   val open_tag : Tag.t -> std_ppcmds
+   val close_tag : unit -> std_ppcmds
+   val msg_with  : ...
+
+   module Tag
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
diff --git a/dev/doc/style.txt b/dev/doc/style.txt
index 27695a09b..2ee3dadd7 100644
--- a/dev/doc/style.txt
+++ b/dev/doc/style.txt
@@ -1,75 +1,142 @@
-
-<< L'uniformité du style est plus importante que le style lui-même. >>
-(Kernigan & Pike, The Practice of Programming)
-
-Mode Emacs
-==========
-   Tuareg, que l'on trouve ici :  http://www.prism.uvsq.fr/~acohen/tuareg/
-
-   avec le réglage suivant :     (setq tuareg-in-indent 2)
-
-Types récursifs et filtrages
-============================
-   Une barre de séparation y compris sur le premier constructeur
-
-type t =
-  | A 
-  | B of machin
-
-match expr with
-  | A -> ...
-  | B x -> ...
-
-Remarque : à partir de la 8.2 environ, la tendance est à utiliser le
-format suivant qui permet de limiter l'escalade d'indentation tout en
-produisant un aspect visuel intéressant de bloc :
-
-type t =
-| A 
-| B of machin
-
-match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = function
-| A -> ...
-| B x -> ...
-
-Le deuxième cas est obtenu sous tuareg avec les réglages
-
-  (setq tuareg-with-indent 0)
-  (setq tuareg-function-indent 0)
-  (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien 
-                                      /// pour les let mais pas pour les let-in
-
-Conditionnelles
-===============
-  if condition then
-    premier-cas
-  else
-    deuxieme-cas
-
-  Si effets de bord dans les branches, utilisez begin ... end et non des
-  parenthèses i.e.
-
-  if condition then begin
-    instr1;
-    instr2
-  end else begin
-    instr3;
-    instr4
-  end
-    
-  Si la première branche lève une exception, évitez le else i.e.
-
-    if condition then                     if condition then error "machin";
-      error "machin"          ----->      suite
+<< Style uniformity is more important than style itself >>
+   (Kernigan & Pike, The Practice of Programming)
+
+OCaml Style:
+- Spacing and indentation
+  - indent your code (using tuareg default)
+  - no strong constraints in formatting "let in"; possible styles are:
+    "let x = ... in"
+    "let x =
+       ... in"
+    "let
+       x = ...
+     in"
+  - but: no extra indentation before a "in" coming on next line,
+    otherwise, it first shifts further and further on the right,
+    reducing the amount of space available; second, it is not robust to
+    insertion of a new "let"
+  - it is established usage to have space around "|" as in
+    "match c with
+     | [] | [a] -> ...
+     | a::b::l -> ..."
+  - in a one-line "match", it is preferred to have no "|" in front of
+    the first case (this saves spaces for the match to hold in the line)
+  - from about 8.2, the tendency is to use the following format which
+    limit excessive indentation while providing an interesting "block" aspect
+    type t =
+    | A 
+    | B of machin
+
+    let f expr = match expr with
+    | A -> ...
+    | B x -> ...
+
+    let f expr = function
+    | A -> ...
+    | B x -> ...
+  - add spaces around = and == (make the code "breaths")
+  - the common usage is to write "let x,y = ... in ..." rather than
+    "let (x,y) = ... in ..."
+  - parenthesizing with either "(" and ")" or with "begin" and "end" is
+    common practice
+  - preferred layout for conditionals:
+    if condition then
+      premier-cas
     else
-      suite
-
-  
+      deuxieme-cas
+  - in case of effects in branches, use "begin ... end" rather than
+    parentheses
+    if condition then begin
+      instr1;
+      instr2
+    end else begin
+      instr3;
+      instr4
+    end
+  - if the first branch raises an exception, avoid the "else", i.e.:
+    if condition then                     if condition then error "foo";
+      error "foo"          ----->         bar
+    else
+      bar
+  - it is the usage not to use ;; to end OCaml sentences (however,
+    inserting ";;" can be useful for debugging syntax errors crossing
+    the boundary of functions)
+  - relevant options in tuareg:
+    (setq tuareg-in-indent 2)
+    (setq tuareg-with-indent 0)
+    (setq tuareg-function-indent 0)
+    (setq tuareg-let-always-indent nil)
+
+- Coding methodology
+  - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C),
+    Out_of_memory, Stack_overflow, etc.
+    at least, use "try with e when Errors.noncritical e -> ..."
+    (to be detailed, Pierre L. ?)
+  - do not abuse of fancy combinators: sometimes what a "let rec" loop
+    does is more readable and simpler to grasp than what a "fold" does
+  - do not break abstractions: if an internal property is hidden
+    behind an interface, do no rely on it in code which uses this
+    interface (e.g. do not use List.map thinking it is left-to-right,
+    use map_left)
+  - in particular, do not use "=" on abstract types: there is no
+    reason a priori that it is the intended equality on this type; use the
+    "equal" function normally provided with the abstract type
+  - avoid polymorphically typed "=" whose implementation is not
+    optimized in OCaml and which has moreover no reason to be the
+    intended implementation of the equality when it comes to be
+    instantiated on a particular type (e.g. use List.mem_f,
+    List.assoc_f, rather than List.mem, List.assoc, etc, unless it is
+    absolutely clear that "=" will implement the intended equality, and
+    with the right complexity)
+  - any new general-purpose enough combinator on list should be put in
+    cList.ml, on type option in cOpt.ml, etc.
+  - unless of a good reason not to so, follow the style of the
+    surrounding code in the same file as much as possible,
+    the general guidelines are otherwise "let spacing breaths" (we
+    have large screen nowadays), "make your code easy to read and
+    to understand"
+  - document what is tricky, but do not overdocument, sometimes the
+    choice of names and the structuration of the code is a better
+    documentation than a long discourse; use of unicode in comments is
+    welcome if it can make comments more readable (then
+    "toggle-enable-multibyte-characters" can help when using the
+    debugger in emacs)
+  - all of initial "open File", or of small-scope File.(...), or
+    per-ident File.foo are common practices
+
+- Choice of variable names
+  - be consistent when naming from one function to another
+  - be consistent with the naming adopted in the functions from the
+    same file, or with the naming used elsewhere by similar functions
+  - use variable names which express meaning
+  - keep "cst" for constants and avoid it for constructors which is
+    otherwise a source of confusion
+  - for constructors, use "cstr" in type constructor (resp. "cstru" in
+    constructor puniverse); avoid "constr" for "constructor" which
+    could be think as the name of an arbitrary Constr.t
+  - for inductive types, use "ind" in the type inductive (resp "indu"
+    in inductive puniverse)
+  - for env, use "env"
+  - for evar_map, use "sigma", with tolerance into "evm" and "evd"
+  - for named_context or rel_context, use "ctxt" or "ctx" (or "sign")
+  - for formal/actual indices of inductive types: "realdecls", "realargs"
+  - for formal/actual parameters of inductive types: "paramdecls", "paramargs"
+  - for terms, use e.g. c, b, a, ...
+  - if a term is known to be a function: f, ...
+  - if a term is known to be a type: t, u, typ, ...
+  - for a declaration, use d or "decl"
+  - for errors, exceptions, use e
+
+- Common OCaml pitfalls
+  - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in
+    "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in
+    parentheses are needed around the "try" and the inner "match"
+  - even if stream are lazy, the Pp.(++) combinator is strict and
+    forces the evaluation of its arguments (use a "lazy" or a "fun () ->")
+    to make it lazy explicitly
+  - in "if ... then ... else ... ++ ...", the default parenthesizing
+    is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..."
+  - in "let myspecialfun = mygenericfun args", be sure that it does no
+    do side-effect; prefer otherwise "let mygenericfun arg =
+    mygenericfun args arg" to ensure that the function is evaluated at
+    runtime
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 46caca8d6..3850c05fd 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -20,7 +20,7 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
 	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
 	-I $COQTOP/library -I $COQTOP/engine \
-	-I $COQTOP/pretyping -I $COQTOP/parsing \
+	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
@@ -32,6 +32,6 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
 	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
-        -I $COQTOP/plugins/xml \
+        -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
         -I $COQTOP/ide \
 	"$@"
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ac73b54bd..474cc85c1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -29,7 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* std_ppcmds *)
-let pp   x = Pp.pp_with !Pp_control.std_ft x
+let pp   x = Pp.pp_with !Topfmt.std_ft x
 
 (** Future printer *)
 
@@ -235,7 +235,7 @@ let ppenvwithcst e = pp
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
    str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
 
-let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
+let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
 let ppobj obj = Format.print_string (Libobject.object_tag obj)