Merge branch 'v8.7'

13 files changed, 251 insertions, 767 deletions

diff --git a/Makefile.build b/Makefile.build
index 0dafde997..05d751f54 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -101,7 +101,7 @@ DEPENDENCIES := \
 ###########################################################################
 
 # Default timing command
-STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
+STDTIME=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"
 
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
@@ -275,7 +275,7 @@ grammar/grammar.cma : $(GRAMCMO)
 	@touch grammar/test.mlp
 	$(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test
 	@rm -f grammar/test.* grammar/test
-	$(SHOW)'OCAMLC -a $@'   
+	$(SHOW)'OCAMLC -a $@'
 	$(HIDE)$(GRAMC) $^ -linkall -a -o $@
 
 ## Support of Camlp5 and Camlp5
@@ -307,7 +307,7 @@ coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
-	$(SHOW)'COQMKTOP -o $@'	
+	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@
 	$(STRIP) $@
 	$(CODESIGN) $@
@@ -317,7 +317,7 @@ $(COQTOPEXE): $(COQTOPBYTE)
 endif
 
 $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
-	$(SHOW)'COQMKTOP -o $@'	
+	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@
 
 # coqmktop
@@ -667,7 +667,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ;
 %:
 	@echo "Error: no rule to make target $@ (or missing .PHONY)" && false
 
-# For emacs: 
-# Local Variables: 
-# mode: makefile 
+# For emacs:
+# Local Variables:
+# mode: makefile
 # End:
diff --git a/configure.ml b/configure.ml
index c75c3d7e1..9976c19d4 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,7 +11,7 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "trunk"
+let coq_version = "8.7.0~alpha"
 let coq_macos_version = "8.6.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
 let vo_magic = 8691
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 99ec43e41..91337b901 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -91,8 +91,8 @@
 ########################################################################
 # fiat_crypto
 ########################################################################
-: ${fiat_crypto_CI_BRANCH:=less_init_plugins}
-: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
+: ${fiat_crypto_CI_BRANCH:=master}
+: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
 
 ########################################################################
 # formal-topology
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 0dd904648..4cfe0911b 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -9,4 +9,5 @@ opam install -j ${NJOBS} -y menhir
 git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
 
 # Patch to avoid the upper version limit
-( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make )
+( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make )
+
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
deleted file mode 100644
index 43bd2419f..000000000
--- a/doc/refman/RefMan-ind.tex
+++ /dev/null
@@ -1,510 +0,0 @@
-
-%\documentstyle[11pt]{article}
-%\input{title}
-
-%\include{macros}
-%\makeindex
-
-%\begin{document}
-%\coverpage{The module {\tt Equality}}{Cristina CORNES}
-
-%\tableofcontents
-
-\chapter[Tactics for inductive types and families]{Tactics for inductive types and families\label{Addoc-equality}}
-
-This chapter details a few special tactics useful for inferring facts
-from inductive hypotheses. They can be considered as tools that
-macro-generate complicated uses of the basic elimination tactics for
-inductive types. 
-
-Sections \ref{inversion_introduction} to \ref{inversion_using}  present
-inversion tactics and Section~\ref{scheme} describes
-a command {\tt Scheme} for automatic generation of induction schemes
-for mutual inductive types.
-
-%\end{document}
-%\documentstyle[11pt]{article}
-%\input{title}
-
-%\begin{document}
-%\coverpage{Module Inv: Inversion Tactics}{Cristina CORNES}
-
-\section[Generalities about inversion]{Generalities about inversion\label{inversion_introduction}}
-When working with (co)inductive predicates, we are very often faced to
-some of these situations:
-\begin{itemize}
-\item we have an inconsistent instance of an inductive predicate in the
-  local context of hypotheses. Thus, the current goal can be trivially
-  proved by absurdity. 
-
-\item we have a hypothesis that is an instance of an inductive
-  predicate, and the instance has some variables whose constraints we
-  would like to derive.
-\end{itemize}
-
-The inversion tactics are very useful to simplify the work in these
-cases. Inversion tools can be classified in three groups:
-\begin{enumerate}
-\item tactics for inverting an instance without stocking the inversion
-  lemma in the context: 
-  (\texttt{Dependent})  \texttt{Inversion} and
- (\texttt{Dependent}) \texttt{Inversion\_clear}.
-\item commands for generating and stocking in the context the inversion
-  lemma corresponding to an instance: \texttt{Derive}
-  (\texttt{Dependent}) \texttt{Inversion}, \texttt{Derive}
-  (\texttt{Dependent}) \texttt{Inversion\_clear}.
-\item tactics for inverting an instance using an already defined
-  inversion lemma: \texttt{Inversion \ldots using}.
-\end{enumerate}
-
-These tactics work for inductive types of arity $(\vec{x}:\vec{T})s$ 
-where $s \in \{Prop,Set,Type\}$. Sections \ref{inversion_primitive},
-\ref{inversion_derivation} and \ref{inversion_using} 
-describe respectively each group of tools.
-
-As inversion proofs may be large in size, we recommend the user to
-stock the lemmas whenever the same instance needs to be inverted
-several times.\\
-
-Let's consider the relation \texttt{Le} over natural numbers and the
-following variables:
-
-\begin{coq_eval}
-Restore State "Initial".
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive Le : nat -> nat -> Set :=
-  | LeO : forall n:nat, Le 0%N n
-  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-Variable P : nat -> nat -> Prop.
-Variable Q : forall n m:nat, Le n m -> Prop.
-\end{coq_example*}
-
-For example purposes we defined  \verb+Le: nat->nat->Set+
- but we may have defined
-it \texttt{Le} of type \verb+nat->nat->Prop+ or \verb+nat->nat->Type+.
-
-
-\section[Inverting an instance]{Inverting an instance\label{inversion_primitive}}
-\subsection{The non dependent case}
-\begin{itemize}
-
-\item \texttt{Inversion\_clear} \ident~\\
-\index{Inversion-clear@{\tt Inversion\_clear}}
-  Let the type of \ident~ in the local context be $(I~\vec{t})$,
-  where $I$ is a (co)inductive predicate. Then,
-  \texttt{Inversion} applied to \ident~ derives for each possible
-  constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary
-  conditions that should hold for the instance $(I~\vec{t})$ to be
-  proved by $c_i$. Finally it erases \ident~ from the context.
-
-
-
-For example, consider the goal:
-\begin{coq_eval}
-Lemma ex : forall n m:nat, Le (S n) m -> P n m.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-To prove the goal we may need to reason by cases on \texttt{H} and to 
- derive that \texttt{m}  is necessarily of
-the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$.  
-Deriving these conditions corresponds to prove that the
-only possible constructor of \texttt{(Le (S n) m)}  is
-\texttt{LeS} and that we can invert the 
-\texttt{->} in the type  of \texttt{LeS}.  
-This inversion is possible because \texttt{Le} is the smallest set closed by
-the constructors \texttt{LeO} and \texttt{LeS}.
-
-
-\begin{coq_example}
-inversion_clear H.
-\end{coq_example}
-
-Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)}
-and that the hypothesis \texttt{(Le n m0)} has been added to the
-context.
-
-\item \texttt{Inversion} \ident~\\
-\index{Inversion@{\tt Inversion}}
-  This tactic differs from   {\tt Inversion\_clear} in the fact that
-  it adds the equality constraints in the context and
-  it does not erase  the hypothesis \ident.
-
-
-In the previous example, {\tt Inversion\_clear} 
-has substituted \texttt{m} by \texttt{(S m0)}. Sometimes it is
-interesting to have the equality \texttt{m=(S m0)} in the
-context to use it after. In that case we can use  \texttt{Inversion} that
-does not clear the equalities:
-
-\begin{coq_example*}
-Undo.
-\end{coq_example*}
-\begin{coq_example}
-inversion H.
-\end{coq_example}
-
-\begin{coq_eval}
-Undo.
-\end{coq_eval}
-
-Note that the hypothesis \texttt{(S m0)=m} has been deduced and 
-\texttt{H} has not been cleared from the context.
-
-\end{itemize}
-
-\begin{Variants}
-
-\item \texttt{Inversion\_clear } \ident~ \texttt{in} \ident$_1$ \ldots
-  \ident$_n$\\ 
-\index{Inversion_clear...in@{\tt Inversion\_clear...in}}
-  Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This
-  tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing
-  {\tt Inversion\_clear}.
-
-\item \texttt{Inversion } \ident~ \texttt{in} \ident$_1$ \ldots \ident$_n$\\
-\index{Inversion ... in@{\tt Inversion ... in}}
-  Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This
-  tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing
-  \texttt{Inversion}.
-
-
-\item \texttt{Simple Inversion} \ident~ \\
-\index{Simple Inversion@{\tt Simple Inversion}}
-  It is a very primitive inversion tactic that derives all the necessary
-  equalities  but it does not simplify
-  the  constraints as \texttt{Inversion} and
-  {\tt Inversion\_clear} do.
-
-\end{Variants}
-
-
-\subsection{The dependent case}
-\begin{itemize}
-\item \texttt{Dependent Inversion\_clear} \ident~\\
-\index{Dependent Inversion-clear@{\tt Dependent Inversion\_clear}}
-  Let the type of \ident~ in the local context be $(I~\vec{t})$,
-  where $I$ is a (co)inductive predicate, and let the goal  depend both on
-  $\vec{t}$ and \ident. Then, 
-  \texttt{Dependent Inversion\_clear} applied to \ident~ derives 
-   for each possible constructor $c_i$ of $(I~\vec{t})$, {\bf all} the
-  necessary conditions that should hold for the instance $(I~\vec{t})$ to be
-  proved by $c_i$. It also substitutes  \ident~ for the corresponding
-  term  in the goal and  it erases \ident~ from the context.
-
-
-For example, consider the  goal:
-\begin{coq_eval}
-Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-As \texttt{H} occurs in the goal, we may want to reason by cases on its
-structure and so, we would like  inversion tactics to
-substitute \texttt{H} by the corresponding term in constructor form. 
-Neither \texttt{Inversion} nor  {\tt Inversion\_clear} make such a
-substitution. To have such a behavior we use the dependent inversion tactics:
-
-\begin{coq_example}
-dependent inversion_clear H.
-\end{coq_example}
-
-Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
-\texttt{m} by \texttt{(S m0)}.
-
-
-\end{itemize}
-
-\begin{Variants}
-
-\item \texttt{Dependent Inversion\_clear } \ident~ \texttt{ with } \term\\
-\index{Dependent Inversion_clear...with@{\tt Dependent Inversion\_clear...with}}
- \noindent Behaves as \texttt{Dependent Inversion\_clear} but allows giving
-  explicitly the good generalization of the goal. It is useful when
-  the system fails to generalize the goal automatically. If
-  \ident~ has type $(I~\vec{t})$ and $I$ has type
-  $(\vec{x}:\vec{T})s$,   then \term~  must be of type
-  $I:(\vec{x}:\vec{T})(I~\vec{x})\rightarrow s'$ where $s'$ is the
-  type of the goal.
-
-
-
-\item \texttt{Dependent Inversion} \ident~\\
-\index{Dependent Inversion@{\tt Dependent Inversion}}
- This tactic differs from   \texttt{Dependent Inversion\_clear} in the fact that
-  it also  adds the equality constraints in the context and
-  it does not erase  the hypothesis \ident~.
-
-\item \texttt{Dependent Inversion } \ident~ \texttt{ with } \term \\
-\index{Dependent Inversion...with@{\tt Dependent Inversion...with}}
-  Analogous to \texttt{Dependent Inversion\_clear .. with..} above. 
-\end{Variants}
-
-
-
-\section[Deriving the inversion lemmas]{Deriving the inversion lemmas\label{inversion_derivation}}
-\subsection{The non dependent case}
-
-The tactics (\texttt{Dependent}) \texttt{Inversion} and (\texttt{Dependent})
-{\tt Inversion\_clear} work on a
-certain instance $(I~\vec{t})$ of an inductive predicate. At each
-application, they inspect the given instance and derive the
-corresponding inversion lemma.  If we have to invert the same
-instance several times it is recommended to stock the lemma in the
-context and to reuse it whenever we need it.
-
-The families of commands \texttt{Derive Inversion}, \texttt{Derive
-Dependent Inversion}, \texttt{Derive} \\ {\tt Inversion\_clear} and \texttt{Derive Dependent Inversion\_clear}
-allow to generate inversion lemmas for given instances and sorts.  Next
-section describes the tactic \texttt{Inversion}$\ldots$\texttt{using} that refines the
-goal with a specified inversion lemma.
-
-\begin{itemize}
-
-\item \texttt{Derive Inversion\_clear} \ident~ \texttt{with}
-  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ 
-\index{Derive Inversion_clear...with@{\tt Derive Inversion\_clear...with}}
-  Let $I$ be an inductive predicate and $\vec{x}$ the variables
-  occurring in $\vec{t}$. This command generates and stocks
-  the inversion lemma for the sort  \sort~  corresponding to the instance
-  $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf
-    global} environment. When applied it is equivalent to have
-  inverted the instance with the tactic {\tt Inversion\_clear}.
-
-
-  For example, to generate the inversion lemma for the instance
- \texttt{(Le (S n) m)} and the sort \texttt{Prop} we do:
-\begin{coq_example}
-Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort
- Prop.
-\end{coq_example}
-
-Let us  inspect the type of the generated lemma:
-\begin{coq_example}
-Check leminv.
-\end{coq_example}
-
-
-
-\end{itemize}
-
-%\variants
-%\begin{enumerate} 
-%\item \verb+Derive Inversion_clear+  \ident$_1$ \ident$_2$ \\ 
-%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}}
-%  Let \ident$_1$ have type $(I~\vec{t})$ in the local context ($I$
-%  an inductive predicate).  Then, this command has the same semantics
-%  as \verb+Derive Inversion_clear+ \ident$_2$~ \verb+with+
-%  $(\vec{x}:\vec{T})(I~\vec{t})$ \verb+Sort Prop+ where $\vec{x}$ are the free
-%  variables of $(I~\vec{t})$ declared in the local context (variables
-%  of the global context are considered as constants). 
-%\item \verb+Derive Inversion+ \ident$_1$~ \ident$_2$~\\
-%\index{Derive Inversion@{\tt Derive Inversion}}
-% Analogous to the previous command. 
-%\item \verb+Derive Inversion+ $num$ \ident~ \ident~ \\ 
-%\index{Derive Inversion@{\tt Derive Inversion}}
-%  This command behaves as \verb+Derive Inversion+ \ident~ {\it
-%    namehyp} performed on the goal number $num$.
-%
-%\item \verb+Derive Inversion_clear+ $num$ \ident~ \ident~ \\ 
-%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}}
-%  This command behaves as \verb+Derive Inversion_clear+ \ident~
-%  \ident~ performed on the goal number $num$.
-%\end{enumerate}
-
-
-
-A derived inversion lemma is  adequate for inverting the instance
-with which it was generated,  \texttt{Derive} applied to
-different instances yields different lemmas. In general, if we generate
-the inversion lemma with 
-an instance $(\vec{x}:\vec{T})(I~\vec{t})$ and a sort $s$,  the inversion lemma will
-expect a predicate of type $(\vec{x}:\vec{T})s$ as first argument. \\
-
-\begin{Variant}
-\item \texttt{Derive Inversion} \ident~ \texttt{with} 
-  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort\\ 
-\index{Derive Inversion...with@{\tt Derive Inversion...with}}
-     Analogous of \texttt{Derive Inversion\_clear .. with ..} but 
- when applied it is equivalent to having
-  inverted the instance with the tactic \texttt{Inversion}.
-\end{Variant}
-
-\subsection{The dependent case}
-\begin{itemize}
-\item \texttt{Derive Dependent Inversion\_clear} \ident~ \texttt{with}
-  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ 
-\index{Derive Dependent Inversion\_clear...with@{\tt Derive Dependent Inversion\_clear...with}}
-  Let $I$ be an inductive predicate. This command generates and stocks
-  the dependent inversion lemma for the sort  \sort~  corresponding to the instance
-  $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf
-    global} environment. When applied it is equivalent to having
-  inverted the instance with the tactic \texttt{Dependent Inversion\_clear}.
-\end{itemize}
-
-\begin{coq_example}
-Derive Dependent Inversion_clear leminv_dep with
- (forall n m:nat, Le (S n) m) Sort Prop.
-\end{coq_example}
-
-\begin{coq_example}
-Check leminv_dep.
-\end{coq_example}
-
-\begin{Variants}
-\item \texttt{Derive Dependent Inversion} \ident~ \texttt{with}
-  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ 
-\index{Derive Dependent Inversion...with@{\tt Derive Dependent Inversion...with}}
-  Analogous to \texttt{Derive Dependent Inversion\_clear}, but when
-  applied  it is equivalent to having
-  inverted the instance with the tactic \texttt{Dependent Inversion}.
-
-\end{Variants}
-
-\section[Using already defined inversion  lemmas]{Using already defined inversion  lemmas\label{inversion_using}}
-\begin{itemize}
-\item \texttt{Inversion} \ident \texttt{ using} \ident$'$ \\
-\index{Inversion...using@{\tt Inversion...using}}
-  Let \ident~ have type $(I~\vec{t})$ ($I$ an inductive
-  predicate) in the local context, and \ident$'$ be a (dependent) inversion
-  lemma. Then, this tactic refines the current goal with the specified
-  lemma. 
-
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-\begin{coq_example}
-inversion H using leminv.
-\end{coq_example}
-
-
-\end{itemize}
-\variant
-\begin{enumerate}
-\item \texttt{Inversion} \ident~ \texttt{using} \ident$'$ \texttt{in} \ident$_1$\ldots \ident$_n$\\
-\index{Inversion...using...in@{\tt Inversion...using...in}}
-This tactic behaves as generalizing  \ident$_1$\ldots \ident$_n$,
-then doing \texttt{Use Inversion} \ident~\ident$'$.
-\end{enumerate}
-
-\section[\tt Scheme ...]{\tt Scheme ...\index{Scheme@{\tt Scheme}}\label{Scheme}
-\label{scheme}}
-The {\tt Scheme} command is a high-level tool for generating
-automatically (possibly mutual) induction principles for given types
-and sorts.  Its syntax follows the schema :
-
-\noindent
-{\tt Scheme {\ident$_1$} := Induction for \term$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} .. \\
-        with {\ident$_m$} := Induction for {\term$_m$} Sort
-        {\sort$_m$}}\\
-\term$_1$ \ldots \term$_m$ are different inductive types belonging to
-the same package of mutual inductive definitions. This command
-generates {\ident$_1$}\ldots{\ident$_m$} to be mutually recursive
-definitions. Each term {\ident$_i$} proves a general principle 
-of mutual induction for objects in type {\term$_i$}. 
-
-\Example
-The definition of principle of mutual induction for {\tt tree} and
-{\tt forest} over the sort {\tt Set} is defined by the command:
-\begin{coq_eval}
-Restore State "Initial".
-Variables A B : Set.
-Inductive tree : Set :=
-    node : A -> forest -> tree
-with forest : Set :=
-  | leaf : B -> forest
-  | cons : tree -> forest -> forest.
-\end{coq_eval}
-\begin{coq_example*}
-Scheme tree_forest_rec := Induction for tree
-  Sort Set
-  with forest_tree_rec := Induction for forest Sort Set.
-\end{coq_example*}
-You may now look at the type of {\tt tree\_forest\_rec} :
-\begin{coq_example}
-Check tree_forest_rec.
-\end{coq_example}
-This principle involves two different predicates for {\tt trees} and
-{\tt forests}; it also has three premises each one corresponding to a
-constructor of one of the inductive definitions.
-
-The principle {\tt tree\_forest\_rec} shares exactly the same
-premises, only the conclusion now refers to the property of forests.
-\begin{coq_example}
-Check forest_tree_rec.
-\end{coq_example}
-
-\begin{Variant}
-\item {\tt Scheme {\ident$_1$} := Minimality for \term$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} .. \\
-        with {\ident$_m$} := Minimality for {\term$_m$} Sort
-        {\sort$_m$}}\\
-Same as before but defines a non-dependent elimination principle more
-natural in case of inductively defined relations. 
-\end{Variant}
-
-\Example
-With the predicates {\tt odd} and {\tt even} inductively defined as:
-% \begin{coq_eval}
-% Restore State "Initial".
-% \end{coq_eval}
-\begin{coq_example*}
-Inductive odd : nat -> Prop :=
-    oddS : forall n:nat, even n -> odd (S n)
-with even : nat -> Prop :=
-  | evenO : even 0%N
-  | evenS : forall n:nat, odd n -> even (S n).
-\end{coq_example*}
-The following command generates a powerful elimination
-principle:
-\begin{coq_example*}
-Scheme odd_even := Minimality for   odd Sort Prop
-  with even_odd := Minimality for even Sort Prop.
-\end{coq_example*}
-The type of {\tt odd\_even} for instance will be:
-\begin{coq_example}
-Check odd_even.
-\end{coq_example}
-The type of {\tt even\_odd} shares the same premises but the
-conclusion is {\tt (n:nat)(even n)->(Q n)}.
-
-\subsection[\tt Combined Scheme ...]{\tt Combined Scheme ...\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme}
-\label{combinedscheme}}
-The {\tt Combined Scheme} command is a tool for combining 
-induction principles generated by the {\tt Scheme} command.
-Its syntax follows the schema :
-
-\noindent
-{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\
-\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
-the same package of mutual inductive principle definitions. This command
-generates {\ident$_0$} to be the conjunction of the principles: it is
-build from the common premises of the principles and concluded by the
-conjunction of their conclusions. For exemple, we can combine the
-induction principles for trees and forests:
-
-\begin{coq_example*}
-Combined Scheme tree_forest_mutind from tree_ind, forest_ind.
-Check tree_forest_mutind.
-\end{coq_example*}
-
-%\end{document}
-
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 30b6304c1..8337b1c48 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -23,7 +23,7 @@ of Inductive Constructions. It allows the interactive construction of
 formal proofs, and also the manipulation of functional programs 
 consistently with their specifications. It runs as a computer program
 on many architectures.
-%, and mainly on Unix machines. 
+
 It is available with a variety of user interfaces. The present
 document does not attempt to present a comprehensive view of all the
 possibilities of \Coq, but rather to present in the most elementary
@@ -33,63 +33,34 @@ proof tools.  For more advanced information, the reader could refer to
 the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y.
 Bertot and P. Castéran on practical uses of the \Coq{} system.
 
-Coq can be used from a standard teletype-like shell window but
-preferably through the graphical user interface
-CoqIde\footnote{Alternative graphical interfaces exist: Proof General
-and Pcoq.}.
-
 Instructions on installation procedures, as well as more comprehensive
 documentation, may be found in the standard distribution of \Coq,
-which may be obtained from \Coq{} web site \url{https://coq.inria.fr/}.
-
-In the following, we assume that \Coq{} is called from a standard
-teletype-like shell window. All examples preceded by the prompting
-sequence \verb:Coq < : represent user input, terminated by a
-period. 
-
-The following lines usually show \Coq's answer as it appears on the
-users screen. When used from a graphical user interface such as
-CoqIde, the prompt is not displayed: user input is given in one window
+which may be obtained from \Coq{} web site
+\url{https://coq.inria.fr/}\footnote{You can report any bug you find
+while using \Coq{} at \url{https://coq.inria.fr/bugs}. Make sure to
+always provide a way to reproduce it and to specify the exact version
+you used. You can get this information by running \texttt{coqc -v}}.
+\Coq{} is distributed together with a graphical user interface called
+CoqIDE. Alternative interfaces exist such as
+Proof General\footnote{See \url{https://proofgeneral.github.io/}.}.
+
+In the following examples, lines preceded by the prompt \verb:Coq < :
+represent user input, terminated by a period.
+The following lines usually show \Coq's answer.
+When used from a graphical user interface such as
+CoqIDE, the prompt is not displayed: user input is given in one window
 and \Coq's answers are displayed in a different window.
 
-The sequence of such examples is a valid \Coq{}
-session, unless otherwise specified. This version of the tutorial has
-been prepared on a PC workstation running Linux.  The standard
-invocation of \Coq{} delivers a message such as:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-unix:~> coqtop
-Welcome to Coq 8.2 (January 2009)
-
-Coq < 
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-The first line gives a banner stating the precise version of \Coq{}
-used. You should always return this banner when you report an anomaly
-to our bug-tracking system
-\url{https://coq.inria.fr/bugs/}.
-
 \chapter{Basic Predicate Calculus}
 
 \section{An overview of the specification language Gallina}
 
 A formal development in Gallina consists in a sequence of {\sl declarations}
-and {\sl definitions}. You may also send \Coq{} {\sl commands} which are
-not really part of the formal development, but correspond to information
-requests, or service routine invocations. For instance, the command:
-\begin{verbatim}
-Coq < Quit.
-\end{verbatim}
-terminates the current session.
+and {\sl definitions}.
 
 \subsection{Declarations}
 
-A declaration associates a {\sl name} with 
-a {\sl specification}. 
+A declaration associates a {\sl name} with a {\sl specification}.
 A name corresponds roughly to an identifier in a programming
 language, i.e. to a string of letters, digits, and a few ASCII symbols like
 underscore (\verb"_") and prime (\verb"'"), starting with a letter. 
@@ -165,25 +136,25 @@ in the current context:
 Check gt.
 \end{coq_example}
 
-which tells us that \verb:gt: is a function expecting two arguments of
-type \verb:nat: in order to build a logical proposition.
+which tells us that \texttt{gt} is a function expecting two arguments of
+type \texttt{nat} in order to build a logical proposition.
 What happens here is similar to what we are used to in a functional
-programming language: we may compose the (specification) type \verb:nat:
-with the (abstract) type \verb:Prop: of logical propositions through the
+programming language: we may compose the (specification) type \texttt{nat}
+with the (abstract) type \texttt{Prop} of logical propositions through the
 arrow function constructor, in order to get a functional type
-\verb:nat->Prop::
+\texttt{nat -> Prop}:
 \begin{coq_example}
 Check (nat -> Prop).
 \end{coq_example}
-which may be composed one more times with \verb:nat: in order to obtain the
-type \verb:nat->nat->Prop: of binary relations over natural numbers.
-Actually the type \verb:nat->nat->Prop: is an abbreviation for 
-\verb:nat->(nat->Prop):. 
+which may be composed once more with \verb:nat: in order to obtain the
+type \texttt{nat -> nat -> Prop} of binary relations over natural numbers.
+Actually the type \texttt{nat -> nat -> Prop} is an abbreviation for 
+\texttt{nat -> (nat -> Prop)}.
 
 Functional notions may be composed in the usual way. An expression $f$
 of type $A\ra B$ may be applied to an expression $e$ of type $A$ in order
 to form the expression $(f~e)$ of type $B$. Here we get that
-the expression \verb:(gt n): is well-formed of type \verb:nat->Prop:,
+the expression \verb:(gt n): is well-formed of type \texttt{nat -> Prop},
 and thus that the expression \verb:(gt n O):, which abbreviates
 \verb:((gt n) O):, is a well-formed proposition.
 \begin{coq_example}
@@ -193,11 +164,12 @@ Check gt n O.
 \subsection{Definitions}
 
 The initial prelude contains a few arithmetic definitions:
-\verb:nat: is defined as a mathematical collection (type \verb:Set:), constants
-\verb:O:, \verb:S:, \verb:plus:, are defined as objects of types
-respectively \verb:nat:, \verb:nat->nat:, and \verb:nat->nat->nat:.
+\texttt{nat} is defined as a mathematical collection (type \texttt{Set}),
+constants \texttt{O}, \texttt{S}, \texttt{plus}, are defined as objects of
+types respectively \texttt{nat}, \texttt{nat -> nat}, and \texttt{nat ->
+nat -> nat}.
 You may introduce new definitions, which link a name to a well-typed value.
-For instance, we may introduce the constant \verb:one: as being defined
+For instance, we may introduce the constant \texttt{one} as being defined
 to be equal to the successor of zero:
 \begin{coq_example}
 Definition one := (S O).
@@ -217,17 +189,18 @@ argument \verb:m: of type \verb:nat: in order to build its result as
 \verb:(plus m m)::
 
 \begin{coq_example}
-Definition double (m:nat) := plus m m.
+Definition double (m : nat) := plus m m.
 \end{coq_example}
 This introduces the constant \texttt{double} defined as the
-expression \texttt{fun m:nat => plus m m}.
-The abstraction introduced by \texttt{fun} is explained as follows. The expression
-\verb+fun x:A => e+ is well formed of type \verb+A->B+ in a context
-whenever the expression \verb+e+ is well-formed of type \verb+B+ in 
-the given context to which we add the declaration that \verb+x+
-is of type \verb+A+. Here \verb+x+ is a bound, or dummy variable in
-the expression \verb+fun x:A => e+. For instance we could as well have
-defined \verb:double: as \verb+fun n:nat => (plus n n)+.
+expression \texttt{fun m : nat => plus m m}.
+The abstraction introduced by \texttt{fun} is explained as follows.
+The expression \texttt{fun x : A => e} is well formed of type
+\texttt{A -> B} in a context whenever the expression \texttt{e} is
+well-formed of type \texttt{B} in the given context to which we add the
+declaration that \texttt{x} is of type \texttt{A}. Here \texttt{x} is a
+bound, or dummy variable in the expression \texttt{fun x : A => e}.
+For instance we could as well have defined \texttt{double} as
+\texttt{fun n : nat => (plus n n)}.
 
 Bound (local) variables and free (global) variables may be mixed.
 For instance, we may define the function which adds the constant \verb:n:
@@ -243,19 +216,17 @@ Binding operations are well known for instance in logic, where they
 are called quantifiers.  Thus we may universally quantify a
 proposition such as $m>0$ in order to get a universal proposition
 $\forall m\cdot m>0$. Indeed this operator is available in \Coq, with
-the following syntax: \verb+forall m:nat, gt m O+. Similarly to the
+the following syntax: \texttt{forall m : nat, gt m O}. Similarly to the
 case of the functional abstraction binding, we are obliged to declare
 explicitly the type of the quantified variable. We check:
 \begin{coq_example}
-Check (forall m:nat, gt m 0).
-\end{coq_example}
-We may revert to the clean state of
-our initial session using the \Coq{} \verb:Reset: command:
-\begin{coq_example}
-Reset Initial.
+Check (forall m : nat, gt m 0).
 \end{coq_example}
+
 \begin{coq_eval}
+Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \section{Introduction to the proof engine: Minimal Logic}
@@ -340,17 +311,12 @@ the current goal is solvable from the current local assumptions:
 assumption.
 \end{coq_example}
 
-The proof is now finished. We may either discard it, by using the
-command \verb:Abort: which returns to the standard \Coq{} toplevel loop
-without further ado, or else save it as a lemma in the current context,
-under name say \verb:trivial_lemma::
+The proof is now finished. We are now going to ask \Coq{}'s kernel
+to check and save the proof.
 \begin{coq_example}
-Save trivial_lemma.
+Qed.
 \end{coq_example}
 
-As a comment, the system shows the proof script listing all tactic
-commands used in the proof. 
-
 Let us redo the same proof with a few variations. First of all we may name
 the initial goal as a conjectured lemma:
 \begin{coq_example}
@@ -383,46 +349,30 @@ We may thus complete the proof of \verb:distr_impl: with one composite tactic:
 apply H; [ assumption | apply H0; assumption ].
 \end{coq_example}
 
-Let us now save lemma \verb:distr_impl::
-\begin{coq_example}
-Qed.
-\end{coq_example}
-
-Here \verb:Qed: needs no argument, since we gave the name \verb:distr_impl: 
-in advance.
+You should be aware however that relying on automatically generated names is
+not robust to slight updates to this proof script. Consequently, it is
+discouraged in finished proof scripts. As for the composition of tactics with
+\texttt{:} it may hinder the readability of the proof script and it is also
+harder to see what's going on when replaying the proof because composed
+tactics are evaluated in one go.
 
 Actually, such an easy combination of tactics \verb:intro:, \verb:apply:
 and \verb:assumption: may be found completely automatically by an automatic
 tactic, called \verb:auto:, without user guidance:
-\begin{coq_example}
-Lemma distr_imp : (A -> B -> C) -> (A -> B) -> A -> C.
-auto.
-\end{coq_example}
-
-This time, we do not save the proof, we just discard it with the \verb:Abort: 
-command:
 
-\begin{coq_example}
+\begin{coq_eval}
 Abort.
+\end{coq_eval}
+\begin{coq_example}
+Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
+auto.
 \end{coq_example}
 
-At any point during a proof, we may use \verb:Abort: to exit the proof mode
-and go back to Coq's main loop. We may also use \verb:Restart: to restart
-from scratch the proof of the same lemma. We may also use \verb:Undo: to
-backtrack one step, and more generally \verb:Undo n: to
-backtrack n steps.
-
-We end this section by showing a useful command, \verb:Inspect n.:,
-which inspects the global \Coq{} environment, showing the last \verb:n: declared
-notions: 
+Let us now save lemma \verb:distr_impl::
 \begin{coq_example}
-Inspect 3.
+Qed.
 \end{coq_example}
 
-The declarations, whether global parameters or axioms, are shown preceded by 
-\verb:***:; definitions and lemmas are stated with their specification, but
-their value (or proof-term) is omitted.
-
 \section{Propositional Calculus}
 
 \subsection{Conjunction}
@@ -438,7 +388,7 @@ connective. Let us show how to use these ideas for the propositional connectives
 
 \begin{coq_example}
 Lemma and_commutative : A /\ B -> B /\ A.
-intro.
+intro H.
 \end{coq_example}
 
 We make use of the conjunctive hypothesis \verb:H: with the \verb:elim: tactic,
@@ -453,8 +403,11 @@ conjunctive goal into the two subgoals:
 split.
 \end{coq_example}
 and the proof is now trivial. Indeed, the whole proof is obtainable as follows:
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
+Lemma and_commutative : A /\ B -> B /\ A.
 intro H; elim H; auto.
 Qed.
 \end{coq_example}
@@ -465,7 +418,7 @@ conjunction introduction operator \verb+conj+
 Check conj.
 \end{coq_example}
 
-Actually, the tactic \verb+Split+ is just an abbreviation for \verb+apply conj.+
+Actually, the tactic \verb+split+ is just an abbreviation for \verb+apply conj.+
 
 What we have just seen is that the \verb:auto: tactic is more powerful than
 just a simple application of local hypotheses; it tries to apply as well 
@@ -498,6 +451,17 @@ clear away unnecessary hypotheses which may clutter your screen.
 clear H.
 \end{coq_example}
 
+The tactic \verb:destruct: combines the effects of \verb:elim:, \verb:intros:,
+and \verb:clear::
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+\begin{coq_example}
+Lemma or_commutative : A \/ B -> B \/ A.
+intros H; destruct H.
+\end{coq_example}
+
 The disjunction connective has two introduction rules, since \verb:P\/Q:
 may be obtained from \verb:P: or from \verb:Q:; the two corresponding
 proof constructors are called respectively \verb:or_introl: and
@@ -528,8 +492,11 @@ such a simple tautology. The reason is that we want to keep
 
 A complete tactic for propositional
 tautologies is indeed available in \Coq{} as the \verb:tauto: tactic.
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
+Lemma or_commutative : A \/ B -> B \/ A.
 tauto.
 Qed.
 \end{coq_example}
@@ -541,8 +508,8 @@ currently defined in the context:
 Print or_commutative.
 \end{coq_example}
 
-It is not easy to understand the notation for proof terms without a few
-explanations. The \texttt{fun} prefix, such as \verb+fun H:A\/B =>+, 
+It is not easy to understand the notation for proof terms without some
+explanations. The \texttt{fun} prefix, such as \verb+fun H : A\/B =>+, 
 corresponds
 to \verb:intro H:, whereas a subterm such as 
 \verb:(or_intror: \verb:B H0):
@@ -572,15 +539,17 @@ Lemma Peirce : ((A -> B) -> A) -> A.
 try tauto.
 \end{coq_example}
 
-Note the use of the \verb:Try: tactical, which does nothing if its tactic
+Note the use of the \verb:try: tactical, which does nothing if its tactic
 argument fails.
 
 This may come as a surprise to someone familiar with classical reasoning. 
 Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for 
 every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation
 of Peirce's law may be proved in \Coq{} using \verb:tauto::
-\begin{coq_example}
+\begin{coq_eval}
 Abort.
+\end{coq_eval}
+\begin{coq_example}
 Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A).
 tauto.
 Qed.
@@ -651,26 +620,20 @@ function and predicate symbols.
 \subsection{Sections and signatures}
 
 Usually one works in some domain of discourse, over which range the individual 
-variables and function symbols. In \Coq{} we speak in a language with a rich
-variety of types, so me may mix several domains of discourse, in our 
+variables and function symbols. In \Coq{}, we speak in a language with a rich
+variety of types, so we may mix several domains of discourse, in our 
 multi-sorted language. For the moment, we just do a few exercises, over a 
 domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two 
 predicate symbols  \verb:P: and \verb:R: over \verb:D:, of arities 
-respectively 1 and 2. Such abstract entities may be entered in the context
-as global variables. But we must be careful about the pollution of our
-global environment by such declarations. For instance, we have already 
-polluted our \Coq{} session by declaring the variables
-\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:.
+1 and 2, respectively.
 
-\begin{coq_example}
-Reset Initial.
-\end{coq_example}
 \begin{coq_eval}
+Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
-We shall now declare a new \verb:Section:, which will allow us to define
-notions local to a well-delimited scope. We start by assuming a domain of
+We start by assuming a domain of
 discourse \verb:D:, and a binary relation \verb:R:  over \verb:D:: 
 \begin{coq_example}
 Section Predicate_calculus.
@@ -686,18 +649,19 @@ a theory, but rather local hypotheses to a theorem, we open a specific
 section to this effect.
 \begin{coq_example}
 Section R_sym_trans.
-Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
-Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
+Hypothesis R_symmetric : forall x y : D, R x y -> R y x.
+Hypothesis R_transitive :
+    forall x y z : D, R x y -> R y z -> R x z.
 \end{coq_example}
 
-Remark the syntax \verb+forall x:D,+ which stands for universal quantification
+Remark the syntax \verb+forall x : D,+ which stands for universal quantification
 $\forall x : D$.
 
 \subsection{Existential quantification}
 
 We now state our lemma, and enter proof mode.
 \begin{coq_example}
-Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
+Lemma refl_if : forall x : D, (exists y, R x y) -> R x x.
 \end{coq_example}
 
 Remark that the hypotheses which are local to the currently opened sections
@@ -711,13 +675,13 @@ predicate as argument:
 \begin{coq_example}
 Check ex.
 \end{coq_example}
-and the notation \verb+(exists x:D, P x)+ is just concrete syntax for 
-the expression \verb+(ex D (fun x:D => P x))+. 
+and the notation \verb+(exists x : D, P x)+ is just concrete syntax for 
+the expression \verb+(ex D (fun x : D => P x))+. 
 Existential quantification is handled in \Coq{} in a similar
-fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by
+fashion to the connectives \verb:/\: and \verb:\/:: it is introduced by
 the proof combinator \verb:ex_intro:, which is invoked by the specific 
-tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to
-\verb:P:, together with an assumption \verb+h:(P a)+ that indeed \verb+a+
+tactic \verb:exists:, and its elimination provides a witness \verb+a : D+ to
+\verb:P:, together with an assumption \verb+h : (P a)+ that indeed \verb+a+
 verifies \verb:P:. Let us see how this works on this simple example.
 \begin{coq_example}
 intros x x_Rlinked.
@@ -773,8 +737,8 @@ End R_sym_trans.
 All the local hypotheses have been
 discharged in the statement of \verb:refl_if:, which now becomes a general
 theorem in the first-order language declared in section 
-\verb:Predicate_calculus:. In this particular example, the use of section
-\verb:R_sym_trans: has not been really significant, since we could have
+\verb:Predicate_calculus:. In this particular example, section
+\verb:R_sym_trans: has not been really useful, since we could have
 instead stated theorem \verb:refl_if: in its general form, and done 
 basically the same proof, obtaining \verb:R_symmetric: and
 \verb:R_transitive: as local hypotheses by initial \verb:intros: rather
@@ -802,7 +766,7 @@ Lemma weird : (forall x:D, P x) ->  exists a, P a.
 \end{coq_example}
 
 First of all, notice the pair of parentheses around
-\verb+forall x:D, P x+ in
+\verb+forall x : D, P x+ in
 the statement of lemma \verb:weird:.
 If we had omitted them, \Coq's parser would have interpreted the
 statement as a truly trivial fact, since we would 
@@ -820,7 +784,7 @@ systematically inhabited, lemma \verb:weird: only holds in signatures
 which allow the explicit construction of an element in the domain of
 the predicate. 
 
-Let us conclude the proof, in order to show the use of the \verb:Exists:
+Let us conclude the proof, in order to show the use of the \verb:exists:
 tactic:
 \begin{coq_example}
 exists d; trivial.
@@ -836,8 +800,8 @@ We shall need classical reasoning. Instead of loading the \verb:Classical:
 module as we did above, we just state the law of excluded middle as a
 local hypothesis schema at this point:
 \begin{coq_example}
-Hypothesis EM : forall A:Prop, A \/ ~ A.
-Lemma drinker :  exists x:D, P x -> forall x:D, P x.
+Hypothesis EM : forall A : Prop, A \/ ~ A.
+Lemma drinker :  exists x : D, P x -> forall x : D, P x.
 \end{coq_example}
 The proof goes by cases on whether or not
 there is someone who does not drink. Such reasoning by cases proceeds
@@ -847,10 +811,11 @@ proper instance of \verb:EM::
 elim (EM (exists x, ~ P x)).
 \end{coq_example}
 
-We first look at the first case. Let Tom be the non-drinker:
+We first look at the first case. Let Tom be the non-drinker.
+The following combines at once the effect of \verb:intros: and
+\verb:destruct::
 \begin{coq_example}
-intro Non_drinker; elim Non_drinker;
-  intros Tom Tom_does_not_drink.
+intros (Tom, Tom_does_not_drink).
 \end{coq_example}
 
 We conclude in that case by considering Tom, since his drinking leads to
@@ -860,9 +825,10 @@ exists Tom; intro Tom_drinks.
 \end{coq_example}
 
 There are several ways in which we may eliminate a contradictory case;
-a simple one is to use the \verb:absurd: tactic as follows:
+in this case, we use \verb:contradiction: to let \Coq{} find out the
+two contradictory hypotheses:
 \begin{coq_example}
-absurd (P Tom); trivial.
+contradiction.
 \end{coq_example}
 
 We now proceed with the second case, in which actually any person will do;
@@ -904,9 +870,10 @@ Finally, the excluded middle hypothesis is discharged only in
 Note that the name \verb:d: has vanished as well from
 the statements of \verb:weird: and \verb:drinker:, 
 since \Coq's pretty-printer replaces
-systematically a quantification such as \verb+forall d:D, E+, where \verb:d:
-does not occur in \verb:E:, by the functional notation \verb:D->E:. 
-Similarly the name \verb:EM: does not appear in \verb:drinker:. 
+systematically a quantification such as \texttt{forall d : D, E},
+where \texttt{d} does not occur in \texttt{E},
+by the functional notation \texttt{D -> E}.
+Similarly the name \texttt{EM} does not appear in \texttt{drinker}.
 
 Actually, universal quantification, implication, 
 as well as function formation, are
@@ -935,12 +902,12 @@ intros.
 generalize H0.
 \end{coq_example}
 
-Sometimes it may be convenient to use a lemma, although we do not have
-a direct way to appeal to such an already proven fact. The tactic \verb:cut:
-permits to use the lemma at this point, keeping the corresponding proof
-obligation as a new subgoal:
+Sometimes it may be convenient to state an intermediate fact.
+The tactic \verb:assert: does this and introduces a new subgoal
+for this fact to be proved first. The tactic \verb:enough: does
+the same while keeping this goal for later.
 \begin{coq_example}
-cut (R x x); trivial.
+enough (R x x) by auto.
 \end{coq_example}
 We clean the goal by doing an \verb:Abort: command.
 \begin{coq_example*}
@@ -951,10 +918,10 @@ Abort.
 \subsection{Equality}
 
 The basic equality provided in \Coq{} is Leibniz equality, noted infix like
-\verb+x=y+, when \verb:x: and \verb:y: are two expressions of
-type the same Set. The replacement of \verb:x: by \verb:y: in any
-term is effected by a variety of tactics, such as \verb:rewrite:
-and \verb:replace:. 
+\texttt{x = y}, when \texttt{x} and \texttt{y} are two expressions of
+type the same Set. The replacement of \texttt{x} by \texttt{y} in any
+term is effected by a variety of tactics, such as \texttt{rewrite}
+and \texttt{replace}.
 
 Let us give a few examples of equality replacement. Let us assume that
 some arithmetic function \verb:f: is null in zero:
@@ -1009,10 +976,14 @@ In case the equality $t=u$ generated by \verb:replace: $u$ \verb:with:
 $t$ is an assumption
 (possibly modulo symmetry), it will be automatically proved and the
 corresponding goal will not appear. For instance:
-\begin{coq_example}
+
+\begin{coq_eval}
 Restart.
-replace (f 0) with 0.
-rewrite f10; rewrite foo; trivial.
+\end{coq_eval}
+\begin{coq_example}
+Lemma L2 : f (f 1) = 0.
+replace (f 1) with (f 0).
+replace (f 0) with 0; trivial.
 Qed.
 \end{coq_example}
 
@@ -1033,20 +1004,20 @@ predicates over some universe \verb:U:. For instance:
 \begin{coq_example}
 Variable U : Type.
 Definition set := U -> Prop.
-Definition element (x:U) (S:set) := S x.
-Definition subset (A B:set) := 
-  forall x:U, element x A -> element x B.
+Definition element (x : U) (S : set) := S x.
+Definition subset (A B : set) := 
+  forall x : U, element x A -> element x B.
 \end{coq_example}
 
 Now, assume that we have loaded a module of general properties about
 relations over some abstract type \verb:T:, such as transitivity:
 
 \begin{coq_example}
-Definition transitive (T:Type) (R:T -> T -> Prop) :=
-  forall x y z:T, R x y -> R y z -> R x z.
+Definition transitive (T : Type) (R : T -> T -> Prop) :=
+  forall x y z : T, R x y -> R y z -> R x z.
 \end{coq_example}
 
-Now, assume that we want to prove that \verb:subset: is a \verb:transitive:
+We want to prove that \verb:subset: is a \verb:transitive:
 relation. 
 \begin{coq_example}
 Lemma subset_transitive : transitive set subset.
@@ -1071,9 +1042,12 @@ auto.
 \end{coq_example}
 
 Many variations on \verb:unfold: are provided in \Coq. For instance,
-we may selectively unfold one designated occurrence:
-\begin{coq_example}
+instead of unfolding all occurrences of \verb:subset:, we may want to
+unfold only one designated occurrence:
+\begin{coq_eval}
 Undo 2.
+\end{coq_eval}
+\begin{coq_example}
 unfold subset at 2.
 \end{coq_example}
 
@@ -1111,6 +1085,7 @@ are {\sl transparent}.
 \begin{coq_eval}
 Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \section{Data Types as Inductively Defined Mathematical Collections}
@@ -1166,11 +1141,14 @@ right; trivial.
 \end{coq_example}
 
 Indeed, the whole proof can be done with the combination of the
- \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:,
+ \verb:destruct:, which combines \verb:intro: and \verb:elim:,
 with good old \verb:auto::
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
-simple induction b; auto.
+Lemma duality : forall b:bool, b = true \/ b = false.
+destruct b; auto.
 Qed.
 \end{coq_example}
 
@@ -1194,7 +1172,7 @@ Check nat_rec.
 Let us start by showing how to program the standard primitive recursion
 operator \verb:prim_rec: from the more general \verb:nat_rec::
 \begin{coq_example}
-Definition prim_rec := nat_rec (fun i:nat => nat).
+Definition prim_rec := nat_rec (fun i : nat => nat).
 \end{coq_example}
 
 That is, instead of computing for natural \verb:i: an element of the indexed
@@ -1205,22 +1183,27 @@ About prim_rec.
 \end{coq_example}
 
 Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
-get an apparently more complicated expression. Indeed the type of
-\verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may
-be checked in \Coq{} by command \verb:Eval Cbv Beta:, which $\beta$-reduces
-an expression to its {\sl normal form}:
+get an apparently more complicated expression.
+In fact, the two types are convertible and one way of having the proper
+type would be to do some computation before actually defining \verb:prim_rec:
+as such:
+
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+Set Printing Compact Contexts.
+\end{coq_eval}
+
 \begin{coq_example}
-Eval cbv beta in
-  ((fun _:nat => nat) O ->
-   (forall y:nat, 
-      (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
-   forall n:nat, (fun _:nat => nat) n).
+Definition prim_rec :=
+    Eval compute in nat_rec (fun i : nat => nat).
+About prim_rec.
 \end{coq_example}
 
 Let us now show how to program addition with primitive recursion:
 \begin{coq_example}
 Definition addition (n m:nat) :=
-    prim_rec m (fun p rec:nat => S rec) n.
+    prim_rec m (fun p rec : nat => S rec) n.
 \end{coq_example}
 
 That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
@@ -1244,15 +1227,11 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
   end.
 \end{coq_example}
 
-For the rest of the session, we shall clean up what we did so far with 
-types \verb:bool: and \verb:nat:, in order to use the initial definitions
-given in \Coq's \verb:Prelude: module, and not to get confusing error
-messages due to our redefinitions. We thus revert to the initial state:
+\begin{coq_eval}
 \begin{coq_example}
 Reset Initial.
-\end{coq_example}
-\begin{coq_eval}
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \subsection{Simple proofs by induction}
@@ -1261,20 +1240,21 @@ Let us now show how to do proofs by structural induction. We start with easy
 properties of the \verb:plus: function we just defined. Let us first
 show that $n=n+0$.
 \begin{coq_example}
-Lemma plus_n_O : forall n:nat, n = n + 0.
+Lemma plus_n_O : forall n : nat, n = n + 0.
 intro n; elim n.
 \end{coq_example}
 
-What happened was that \verb:elim n:, in order to construct a \verb:Prop:
-(the initial goal) from a \verb:nat: (i.e. \verb:n:), appealed to the
-corresponding induction principle \verb:nat_ind: which we saw was indeed
+What happened was that \texttt{elim n}, in order to construct a \texttt{Prop}
+(the initial goal) from a \texttt{nat} (i.e. \texttt{n}), appealed to the
+corresponding induction principle \texttt{nat\_ind} which we saw was indeed
 exactly Peano's induction scheme. Pattern-matching instantiated the 
-corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get
-as subgoals the corresponding instantiations of the base case \verb:(P O): ,
-and of the inductive step \verb+forall y:nat, P y -> P (S y)+.
-In each case we get an instance of function \verb:plus: in which its second
+corresponding predicate \texttt{P} to \texttt{fun n : nat => n = n + 0},
+and we get as subgoals the corresponding instantiations of the base case
+\texttt{(P O)}, and of the inductive step
+\texttt{forall y : nat, P y -> P (S y)}.
+In each case we get an instance of function \texttt{plus} in which its second
 argument starts with a constructor, and is thus amenable to simplification
-by primitive recursion. The \Coq{} tactic \verb:simpl: can be used for
+by primitive recursion. The \Coq{} tactic \texttt{simpl} can be used for
 this purpose:
 \begin{coq_example}
 simpl.
@@ -1305,12 +1285,12 @@ We now proceed to the similar property concerning the other constructor
 Lemma plus_n_S : forall n m:nat, S (n + m) = n + S m.
 \end{coq_example}
 
-We now go faster, remembering that tactic \verb:simple induction: does the
+We now go faster, using the tactic \verb:induction:, which does the
 necessary \verb:intros: before applying \verb:elim:. Factoring simplification
 and automation in both cases thanks to tactic composition, we prove this
 lemma in one line:
 \begin{coq_example}
-simple induction n; simpl; auto.
+induction n; simpl; auto.
 Qed.
 Hint Resolve plus_n_S .
 \end{coq_example}
@@ -1324,7 +1304,7 @@ Lemma plus_com : forall n m:nat, n + m = m + n.
 Here we have a choice on doing an induction on \verb:n: or on \verb:m:, the
 situation being symmetric. For instance:
 \begin{coq_example}
-simple induction m; simpl; auto.
+induction m as [ | m IHm ]; simpl; auto.
 \end{coq_example}
 
 Here \verb:auto: succeeded on the base case, thanks to our hint
@@ -1332,7 +1312,7 @@ Here \verb:auto: succeeded on the base case, thanks to our hint
 \verb:auto: does not handle:
 
 \begin{coq_example}
-intros m' E; rewrite <- E; auto.
+rewrite <- IHm; auto.
 Qed.
 \end{coq_example}
 
@@ -1344,13 +1324,13 @@ the constructors \verb:O: and \verb:S:: it computes to \verb:False:
 when its argument is \verb:O:, and to \verb:True: when its argument is 
 of the form \verb:(S n)::
 \begin{coq_example}
-Definition Is_S (n:nat) := match n with
-                           | O => False
-                           | S p => True
-                           end.
+Definition Is_S (n : nat) := match n with
+                             | O => False
+                             | S p => True
+                             end.
 \end{coq_example}
 
-Now we may use the computational power of \verb:Is_S: in order to prove
+Now we may use the computational power of \verb:Is_S: to prove
 trivially that \verb:(Is_S (S n))::
 \begin{coq_example}
 Lemma S_Is_S : forall n:nat, Is_S (S n).
@@ -1389,8 +1369,11 @@ Actually, a specific tactic \verb:discriminate: is provided
 to produce mechanically such proofs, without the need for the user to define
 explicitly the relevant discrimination predicates:
 
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
+Lemma no_confusion : forall n:nat, 0 <> S n.
 intro n; discriminate.
 Qed.
 \end{coq_example}
@@ -1403,12 +1386,13 @@ may define inductive families, and for instance inductive predicates.
 Here is the definition of predicate $\le$ over type \verb:nat:, as
 given in \Coq's \verb:Prelude: module:
 \begin{coq_example*}
-Inductive le (n:nat) : nat -> Prop :=
+Inductive le (n : nat) : nat -> Prop :=
   | le_n : le n n
-  | le_S : forall m:nat, le n m -> le n (S m).
+  | le_S : forall m : nat, le n m -> le n (S m).
 \end{coq_example*}
 
-This definition introduces a new predicate \verb+le:nat->nat->Prop+,
+This definition introduces a new predicate
+\verb+le : nat -> nat -> Prop+,
 and the two constructors \verb:le_n: and \verb:le_S:, which are the
 defining clauses of \verb:le:. That is, we get not only the ``axioms''
 \verb:le_n: and \verb:le_S:, but also the converse property, that 
@@ -1426,7 +1410,7 @@ Check le_ind.
 Let us show how proofs may be conducted with this principle.
 First we show that $n\le m \Rightarrow n+1\le m+1$:
 \begin{coq_example}
-Lemma le_n_S : forall n m:nat, le n m -> le (S n) (S m).
+Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m).
 intros n m n_le_m.
 elim n_le_m.
 \end{coq_example}
@@ -1442,10 +1426,14 @@ intros; apply le_S; trivial.
 
 Now we know that it is a good idea to give the defining clauses as hints,
 so that the proof may proceed with a simple combination of 
-\verb:induction: and \verb:auto:.
+\verb:induction: and \verb:auto:. \verb:Hint Constructors le:
+is just an abbreviation for \verb:Hint Resolve le_n le_S:.
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 \begin{coq_example}
-Restart.
-Hint Resolve le_n le_S .
+Hint Constructors le.
+Lemma le_n_S : forall n m : nat, le n m -> le (S n) (S m).
 \end{coq_example}
 
 We have a slight problem however. We want to say ``Do an induction on
@@ -1453,7 +1441,7 @@ hypothesis \verb:(le n m):'', but we have no explicit name for it. What we
 do in this case is to say ``Do an induction on the first unnamed hypothesis'',
 as follows.
 \begin{coq_example}
-simple induction 1; auto.
+induction 1; auto.
 Qed.
 \end{coq_example}
 
@@ -1483,6 +1471,7 @@ Qed.
 \begin{coq_eval}
 Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 
 \section{Opening library modules}
@@ -1552,6 +1541,7 @@ known lemmas about both the successor and the less or equal relation, just ask:
 \begin{coq_eval}
 Reset Initial.
 Set Printing Width 60.
+Set Printing Compact Contexts.
 \end{coq_eval}
 \begin{coq_example}
 Search S le.
@@ -1562,14 +1552,13 @@ predicate appears at the head position in the conclusion.
 SearchHead le.
 \end{coq_example}
 
-A new and more convenient search tool is \verb:SearchPattern:
-developed by Yves Bertot. It allows finding the theorems with a
-conclusion matching a given pattern, where \verb:_: can be used in
-place of an arbitrary term. We remark in this example, that \Coq{}
+The \verb:Search: commands also allows finding the theorems
+containing a given pattern, where \verb:_: can be used in
+place of an arbitrary term. As shown in this example, \Coq{}
 provides usual infix notations for arithmetic operators.
 
 \begin{coq_example}
-SearchPattern (_ + _ = _).
+Search (_ + _ = _).
 \end{coq_example}
 
 \section{Now you are on your own}
diff --git a/engine/proofview.ml b/engine/proofview.ml
index c542fd976..b4e2160f4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1072,13 +1072,6 @@ module Goal = struct
     end
     end
 
-  exception NotExactlyOneSubgoal
-  let _ = CErrors.register_handler begin function
-  | NotExactlyOneSubgoal ->
-      CErrors.user_err (Pp.str"Not exactly one subgoal.")
-  | _ -> raise CErrors.Unhandled
-  end
-
   let enter_one f =
     let open Proof in
     Comb.get >>= function
@@ -1090,7 +1083,7 @@ module Goal = struct
          let (e, info) = CErrors.push e in
          tclZERO ~info e
       end
-    | _ -> tclZERO NotExactlyOneSubgoal
+    | _ -> assert false (* unsatisfied not-exactly-one-goal precondition *)
 
   let goals =
     Pv.get >>= fun step ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index e98f59f0f..530204501 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -498,7 +498,7 @@ module Goal : sig
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (** Like {!enter}, but assumes exactly one goal under focus, raising *)
-  (** an error otherwise. *)
+  (** a fatal error otherwise. *)
   val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
 
   (** Recover the list of current goals under focus, without evar-normalization.
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 23ac2fed0..7f96627a6 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -181,7 +181,7 @@ module Make (E : EqType) =
     let sz = Weak.length bucket in
     let rec loop i =
       if i >= sz then ifnotfound index
-      else if h = hashes.(i) then begin
+      else if Int.equal h hashes.(i) then begin
         match Weak.get bucket i with
         | Some v when E.eq v d -> v
         | _ -> loop (i + 1)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1cb694da6..4131f9a61 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -189,9 +189,14 @@ let cs_pattern_of_constr t =
 
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
-         (fun (t,con_pp,proji_sp_pp) ->
+         (fun (sign,env,t,con,proji_sp) ->
+          let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
+          let env = Termops.push_rels_assum sign env in
+          let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
+          let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
+          let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in
           strbrk "Projection value has no head constant: "
-          ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance "  
+          ++ term_pp ++ strbrk " in canonical instance "
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
@@ -202,9 +207,9 @@ let compute_canonical_projections warn (con,ind) =
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
-  let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+  let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
   let t = EConstr.Unsafe.to_constr t in
-  let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in
+  let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
@@ -221,9 +226,7 @@ let compute_canonical_projections warn (con,ind) =
 		   let patt, n , args = cs_pattern_of_constr t in
 		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
-                     let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
-                      and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-                     if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
+                   if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);
                    l
 	       end
 	   | _ -> l)
diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out
new file mode 100644
index 000000000..a70f8ca45
--- /dev/null
+++ b/test-suite/output/Warnings.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-22:
+Warning: Projection value has no head constant: fun x : B => x in canonical
+instance a of b, ignoring it. [projection-no-head-constant,typechecker]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
new file mode 100644
index 000000000..7465442ca
--- /dev/null
+++ b/test-suite/output/Warnings.v
@@ -0,0 +1,5 @@
+(* Term in warning was not printed in the right environment at some time *)
+Record A := { B:Type; b:B->B }.
+Definition a B := {| B:=B; b:=fun x => x |}.
+Canonical Structure a.
+
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index c4afc930a..86be54d46 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -62,7 +62,7 @@ VERBOSE ?=
 # Time the Coq process (set to non empty), and how (see default value)
 TIMED?=
 TIMECMD?=
-STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
+STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"
 
 # Coq binaries
 COQC     ?= "$(COQBIN)coqc"