20 files changed, 283 insertions, 110 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
new file mode 100644
index 0000000000..241ec35861
--- /dev/null
+++ b/dev/ci/ci-basic-overlay.sh
@@ -0,0 +1,103 @@
+#!/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
+########################################################################
+: ${HoTT_CI_BRANCH:=mz-8.7}
+: ${HoTT_CI_GITURL:=https://github.com/ejgallego/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}
+
+########################################################################
+# 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 fbcf9be1d6..3f0716511d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -3,7 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color
 Color_CI_DIR=${CI_BUILD_DIR}/color
 
 svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 6f624ab6ec..c94f150263 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -11,9 +11,9 @@ ls `pwd`/bin
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
 
-# Maybe we should just use Ruby...
-mathcomp_CI_BRANCH=master
-mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+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
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 111222ac7f..c78ffdc2c0 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-CompCert_CI_BRANCH=master
-CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
 CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
 
 opam install -j ${NJOBS} -y menhir
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 9dfdb87451..40eff03b78 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-Coquelicot_CI_BRANCH=master
-Coquelicot_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
 Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
 
 install_ssreflect
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 7fc0dae2c0..93d39aab07 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-fiat_crypto_CI_BRANCH=master
-fiat_crypto_CI_GITURL=https://github.com/mit-plv/fiat-crypto.git
 fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
 
 git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 0b3312e878..c62aa1d859 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-fiat_parsers_CI_BRANCH=master
-fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git
 fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
 
 git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 30eca7a3e9..ec19bd9939 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-Flocq_CI_BRANCH=master
-Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
 Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
 
 git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR}
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 7b5950c887..4e5aa2687b 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-GeoCoq_CI_BRANCH=master
-GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
 GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
 
 git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 62733c9452..1bf6e9a872 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-HoTT_CI_BRANCH=mz-8.7
-HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git
 HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
 git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 10f2c2b4bd..eb1d1be078 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -3,12 +3,8 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-stdpp_CI_BRANCH=master
-stdpp_CI_GITURL=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
 stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
 
-Iris_CI_BRANCH=master
-Iris_CI_GITURL=https://gitlab.mpi-sws.org/FP/iris-coq.git
 Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
 
 install_ssreflect
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index e6a57404fe..beb75773b7 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -3,12 +3,8 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-math_classes_CI_BRANCH=v8.6
-math_classes_CI_GITURL=https://github.com/math-classes/math-classes.git
 math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
-Corn_CI_BRANCH=v8.6
-Corn_CI_GITURL=https://github.com/c-corn/corn.git
 Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 # Setup Math-Classes
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 1ea56af29a..e31691179e 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -3,12 +3,7 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-unicoq_CI_BRANCH=master
-unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git
 unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-
-metacoq_CI_BRANCH=master
-metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git
 metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
 # Setup UniCoq
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index c451bf26a1..7d23ccad97 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,7 +3,8 @@
 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-tlc.sh b/dev/ci/ci-tlc.sh
index 415f9b38f9..ce26399378 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-tlc_CI_BRANCH=master
-tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git
 tlc_CI_DIR=${CI_BUILD_DIR}/tlc
 
 git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 4c4b4f1ce1..175b82b5f9 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-UniMath_CI_BRANCH=master
-UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git
 UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
 
 git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
new file mode 100644
index 0000000000..0285747432
--- /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/doc/api.txt b/dev/doc/api.txt
new file mode 100644
index 0000000000..5827257b53
--- /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 8d2d055908..12c3ec4546 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -39,6 +39,8 @@ 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
diff --git a/dev/doc/style.txt b/dev/doc/style.txt
index 27695a09b1..2ee3dadd77 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