Merge branch 'v8.5'

5 files changed, 130 insertions, 132 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index efcc84ee98..11dd3a0517 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -201,7 +201,7 @@ in their context. In this case, the obligations should be transparent
 recursive calls can be checked by the
 kernel's type-checker. There is an optimization in the generation of
 obligations which gets rid of the hypothesis corresponding to the
-functionnal when it is not necessary, so that the obligation can be
+functional when it is not necessary, so that the obligation can be
 declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the
 context, the proof of the obligation is \emph{required} to be declared transparent.
 
@@ -216,7 +216,7 @@ properties. It will generate obligations, try to solve them
 automatically and fail if some unsolved obligations remain. 
 In this case, one can first define the lemma's
 statement using {\tt Program Definition} and use it as the goal afterwards.
-Otherwise the proof will be started with the elobarted version as a goal.
+Otherwise the proof will be started with the elaborated version as a goal.
 The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt
   Hypothesis}, {\tt Axiom} etc...
 
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 3fd5ae0b24..9d79f7cac3 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -109,7 +109,7 @@ sets, namely the sorts {\Set} and {\Type$(j)$} for $j<i$, and all
 products, subsets and function types over these sorts.
 
 Formally, we call {\Sort} the set of sorts which is defined by:
-\[\Sort \equiv \{\Prop,\Set,\Type(i)| i \in \NN\} \]
+\[\Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i \in \NN\} \]
 \index{Type@{\Type}}
 \index{Prop@{\Prop}}
 \index{Set@{\Set}}
@@ -128,7 +128,7 @@ the universe \Type$(i)$. One only writes \Type. The
 system itself generates for each instance of \Type\ a new
 index for the universe and checks that the constraints between these
 indexes can be solved. From the user point of view we consequently
-have {\sf Type :Type}.
+have {\Type}:{\Type}.
 
 We shall make precise in the typing rules the constraints between the
 indexes. 
@@ -140,7 +140,8 @@ identifier with a number) or a successor of an algebraic universe (an
 expression $u+1$), or an upper bound of algebraic universes (an
 expression $max(u_1,...,u_n)$), or the base universe (the expression
 $0$) which corresponds, in the arity of sort-polymorphic inductive
-types, to the predicative sort {\Set}. A graph of constraints between
+types (see Section \ref{Sort-polymorphism-inductive}),
+to the predicative sort {\Set}. A graph of constraints between
 the universe variables is maintained globally. To ensure the existence
 of a mapping of the universes to the positive integers, the graph of
 constraints must remain acyclic.  Typing expressions that violate the
@@ -148,9 +149,10 @@ acyclicity of the graph of constraints results in a \errindex{Universe
 inconsistency} error (see also Section~\ref{PrintingUniverses}).
 
 \subsection{Constants}
-Besides the sorts, the language also contains constants denoting
-objects in the environment. These constants may denote previously
-defined objects but also objects related to inductive definitions
+
+Constants refers to
+objects in the global environment. These constants may denote previously
+defined objects, but also objects related to inductive definitions
 (either the type itself or one of its constructors or destructors).
 
 \medskip\noindent {\bf Remark. } In other presentations of \CIC, 
@@ -174,7 +176,7 @@ in a theory where inductive objects are represented by terms.
 
 \subsection{Terms}
 
-Terms are built from variables, global names, constructors,
+Terms are built from variables, constants, constructors,
 abstraction, application, local declarations bindings (``let-in''
 expressions) and product.
 
@@ -213,7 +215,7 @@ More precisely the language of the {\em Calculus of Inductive
 \end{enumerate}
 
 \paragraph{Notations.} Application associates to the left such that
-$(t~t_1\ldots t_n)$ represents $(\ldots (t~t_1)\ldots t_n)$. The
+$(t\;t_1\;t_2\ldots t_n)$ represents $(\ldots ((t\;t_1)\;t_2)\ldots t_n)$. The
 products and arrows associate to the right such that $\forall~x:A,B\ra C\ra
 D$ represents $\forall~x:A,(B\ra (C\ra D))$.  One uses sometimes
 $\forall~x~y:A,B$ or
@@ -236,33 +238,33 @@ is written $\subst{u}{x}{t}$.
 \section[Typed terms]{Typed terms\label{Typed-terms}}
 
 As objects of type theory, terms are subjected to {\em type
-discipline}. The well typing of a term depends on an environment which
-consists in a global environment (see below) and a local context.
+discipline}. The well typing of a term depends on
+a global environment (see below) and a local context.
 
 \paragraph{Local context.}
-A {\em local context} (or shortly context) is an ordered list of
+A {\em local context} is an ordered list of
 declarations of variables. The declaration of some variable $x$ is
-either an assumption, written $x:T$ ($T$ is a type) or a definition,
-written $x:=t:T$.  We use brackets to write contexts. A
+either a local assumption, written $x:T$ ($T$ is a type) or a local definition,
+written $x:=t:T$.  We use brackets to write local contexts. A
 typical example is $[x:T;y:=u:U;z:V]$.  Notice that the variables
-declared in a context must be distinct. If $\Gamma$ declares some $x$,
+declared in a local context must be distinct. If $\Gamma$ declares some $x$,
 we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that
 either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such
 that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some
-$x:=t:T$, we also write $(x:=t:T) \in \Gamma$.  Contexts must be
-themselves {\em well formed}.  For the rest of the chapter, the
-notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context
+$x:=t:T$, we also write $(x:=t:T) \in \Gamma$.
+For the rest of the chapter, the
+notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the local context
 $\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The
-notation $[]$ denotes the empty context.  \index{Context}
+notation $[]$ denotes the empty local context.  \index{Local context}
 
 % Does not seem to be used further...
 % Si dans l'explication WF(E)[Gamma] concernant les constantes
 % definies ds un contexte
 
-We define the inclusion of two contexts $\Gamma$ and $\Delta$ (written
-as $\Gamma \subset \Delta$) as the property, for all variable $x$,
-type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$
-and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.  
+%We define the inclusion of two local contexts $\Gamma$ and $\Delta$ (written
+%as $\Gamma \subset \Delta$) as the property, for all variable $x$,
+%type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$
+%and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.
 %We write
 % $|\Delta|$ for the length of the context $\Delta$, that is for the number
 % of declarations (assumptions or definitions) in $\Delta$.
@@ -270,22 +272,20 @@ and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.
 A variable $x$ is said to be free in $\Gamma$ if $\Gamma$ contains a
 declaration $y:T$ such that $x$ is free in $T$.
 
-\paragraph[Environment.]{Environment.\index{Environment}}
-Because we are manipulating global declarations (constants and global
-assumptions), we also need to consider a global environment $E$.
+\paragraph[Global environment.]{Global environment.\index{Global environment}}
+%Because we are manipulating global declarations (global constants and global
+%assumptions), we also need to consider a global environment $E$.
 
-An environment is an ordered list of declarations of global
-names. Declarations are either assumptions or ``standard''
-definitions, that is abbreviations for well-formed terms
-but also definitions of inductive objects. In the latter
-case, an object in the environment will define one or more constants
-(that is types and constructors, see Section~\ref{Cic-inductive-definitions}).
+A {\em global environment} is an ordered list of global declarations.
+Global declarations are either global assumptions or global
+definitions, but also declarations of inductive objects. Inductive objects themselves declares both inductive or coinductive types and constructors
+(see Section~\ref{Cic-inductive-definitions}).
 
-An assumption will be represented in the environment as
+A global assumption will be represented in the global environment as
 \Assum{\Gamma}{c}{T} which means that $c$ is assumed of some type $T$
-well-defined in some context $\Gamma$. An (ordinary) definition will
-be represented in the environment as \Def{\Gamma}{c}{t}{T} which means
-that $c$ is a constant which is valid in some context $\Gamma$ whose
+well-defined in some local context $\Gamma$. A global definition will
+be represented in the global environment as \Def{\Gamma}{c}{t}{T} which means
+that $c$ is a constant which is valid in some local context $\Gamma$ whose
 value is $t$ and type is $T$.
 
 The rules for inductive definitions (see section
@@ -295,23 +295,27 @@ declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is
 declared in $E$, we write $(c : T) \in E$.
 
 \paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}}
-In the following, we assume $E$ is a valid environment w.r.t.
-inductive definitions.  We define simultaneously two
+In the following, we define simultaneously two
 judgments.  The first one \WTEG{t}{T} means the term $t$ is well-typed
-and has type $T$ in the environment $E$ and context $\Gamma$.  The
-second judgment \WFE{\Gamma} means that the environment $E$ is
-well-formed and the context $\Gamma$ is a valid context in this
-environment.  It also means a third property which makes sure that any
-constant in $E$ was defined in an environment which is included in
-$\Gamma$
-\footnote{This requirement could be relaxed if we instead introduced
-  an explicit mechanism for instantiating constants. At the external
-  level, the Coq engine works accordingly to this view that all the
-  definitions in the environment were built in a sub-context of the
-  current context.}.
-
-A term $t$ is well typed in an environment $E$ iff there exists a
-context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
+and has type $T$ in the global environment $E$ and local context $\Gamma$.  The
+second judgment \WFE{\Gamma} means that the global environment $E$ is
+well-formed and the local context $\Gamma$ is a valid local context in this
+global environment.
+% HH: This looks to me complicated. I think it would be better to talk
+% about ``discharge'' as a transformation of global environments,
+% rather than as keeping a local context next to global constants.
+%
+%%  It also means a third property which makes sure that any
+%%constant in $E$ was defined in an environment which is included in
+%%$\Gamma$
+%%\footnote{This requirement could be relaxed if we instead introduced
+%%  an explicit mechanism for instantiating constants. At the external
+%%  level, the Coq engine works accordingly to this view that all the
+%%  definitions in the environment were built in a local sub-context of the
+%%  current local context.}.
+
+A term $t$ is well typed in a global environment $E$ iff there exists a
+local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
 be derived from the following rules.
 \begin{description}
 \item[W-E] \inference{\WF{[]}{[]}}
@@ -368,7 +372,7 @@ may be used in a conversion rule (see Section~\ref{conv-rules}).
 We want to be able to identify some terms as we can identify the
 application of a function to a given argument with its result. For
 instance the identity function over a given type $T$ can be written
-$\lb x:T\mto x$. In any environment $E$ and context $\Gamma$, we want to identify any object $a$ (of type $T$) with the
+$\lb x:T\mto x$. In any global environment $E$ and local context $\Gamma$, we want to identify any object $a$ (of type $T$) with the
 application $((\lb x:T\mto x)~a)$. We define for this a {\em reduction} (or a
 {\em conversion}) rule we call $\beta$:
 \[ \WTEGRED{((\lb x:T\mto
@@ -385,7 +389,7 @@ refer the interested reader to \cite{Coq85}.
 
 \paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}}
 A specific conversion rule is associated to the inductive objects in
-the environment.  We shall give later on (see Section~\ref{iotared}) the
+the global environment.  We shall give later on (see Section~\ref{iotared}) the
 precise rules but it just says that a destructor applied to an object
 built from a constructor behaves as expected.  This reduction is
 called $\iota$-reduction and is more precisely studied in
@@ -394,7 +398,7 @@ called $\iota$-reduction and is more precisely studied in
 
 \paragraph[$\delta$-reduction.]{$\delta$-reduction.\label{delta}\index{delta-reduction@$\delta$-reduction}}
 
-We may have defined variables in contexts or constants in the global
+We may have defined variables in local contexts or constants in the global
 environment. It is legal to identify such a reference with its value,
 that is to expand (or unfold) it into its value. This
 reduction is called $\delta$-reduction and shows as follows.
@@ -421,7 +425,7 @@ term $t$ of functional type $\forall x:T, U$ with its so-called
 $\eta$-expansion $\lb x:T\mto (t\ x)$ for $x$ an arbitrary variable
 name fresh in $t$.
 
-The notion of $\eta$-reduction ${\lb x:T\mto (t\ x)}{\triangleright}{t}$
+The notion of $\eta$-reduction ${\lb x:T\mto (t\ x)}{\;\triangleright\;}{t}$
 (for $x$ not occurring in $t$) is not type-sound because of subtyping
 (think about $\lb x:\Type(1)\mto (f x)$ of type $\forall
 x:\Type(1), \Type(1)$ for $f$ of type $\forall x:\Type(2),
@@ -433,12 +437,12 @@ the type. However, $\eta$ can be used as a conversion rule.
 \paragraph[Convertibility.]{Convertibility.\label{convertibility}
 \index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}}
 
-Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the environment $E$ and context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
+Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the global environment $E$ and local context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
 
 We say that two terms $t_1$ and $t_2$ are {\em
   $\beta\iota\delta\zeta\eta$-convertible}, or simply {\em
-  convertible}, or {\em equivalent}, in the environment $E$ and
-context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that
+  convertible}, or {\em equivalent}, in the global environment $E$ and
+local context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that
 $\WTEGRED{t_1}{\triangleright \ldots \triangleright}{u_1}$ and
 $\WTEGRED{t_2}{\triangleright \ldots \triangleright}{u_2}$ and either
 $u_1$ and $u_2$ are identical, or they are convertible up to
@@ -501,10 +505,10 @@ $u_i$ can be reducible.
 Similar notions of head-normal forms involving $\delta$, $\iota$ and $\zeta$
 reductions or any combination of those can also be defined.
 
-\section{Derived rules for environments}
+\section{Derived rules for global environments}
 
 From the original rules of the type system, one can derive new rules
-which change the context of definition of objects in the environment.
+which change the local context of definition of objects in the global environment.
 Because these rules correspond to elementary operations in the \Coq\ 
 engine used in the discharge mechanism at the end of a section, we
 state them explicitly.
@@ -512,9 +516,9 @@ state them explicitly.
 \paragraph{Mechanism of substitution.}
 
 One rule which can be proved valid, is to replace a term $c$ by its
-value in the environment. As we defined the substitution of a term for
+value in the global environment. As we defined the substitution of a term for
 a variable in a term, one can define the substitution of a term for a
-constant. One easily extends this substitution to contexts and
+constant. One easily extends this substitution to local contexts and global
 environments.
 
 \paragraph{Substitution Property:} 
@@ -524,13 +528,13 @@ environments.
 
 \paragraph{Abstraction.}
 
-One can modify the context of definition of a constant $c$ by
+One can modify the local context of definition of a constant $c$ by
 abstracting a constant with respect to the last variable $x$ of its
-defining context. For doing that, we need to check that the constants
+defining local context. For doing that, we need to check that the constants
 appearing in the body of the declaration do not depend on $x$, we need
-also to modify the reference to the constant $c$ in the environment
-and context by explicitly applying this constant to the variable $x$.
-Because of the rules for building environments and terms we know the
+also to modify the reference to the constant $c$ in the global environment
+and local context by explicitly applying this constant to the variable $x$.
+Because of the rules for building global environments and terms we know the
 variable $x$ is available at each stage where $c$ is mentioned.
 
 \paragraph{Abstracting property:} 
@@ -539,13 +543,13 @@ variable $x$ is available at each stage where $c$ is mentioned.
            {\WF{E;\Def{\Gamma}{c}{\lb x:U\mto t}{\forall~x:U,T};
   \subst{F}{c}{(c~x)}}{\subst{\Delta}{c}{(c~x)}}}}
 
-\paragraph{Pruning the context.} 
-We said the judgment \WFE{\Gamma} means that the defining contexts of
+\paragraph{Pruning the local context.}
+We said the judgment \WFE{\Gamma} means that the defining local contexts of
 constants in $E$ are included in $\Gamma$. If one abstracts or
 substitutes the constants with the above rules then it may happen
-that the context $\Gamma$ is now bigger than the one needed for
-defining the constants in $E$. Because defining contexts are growing
-in $E$, the minimum context needed for defining the constants in $E$
+that the local context $\Gamma$ is now bigger than the one needed for
+defining the constants in $E$. Because defining local contexts are growing
+in $E$, the minimum local context needed for defining the constants in $E$
 is the same as the one for the last constant. One can consequently
 derive the following property.
 
@@ -559,8 +563,8 @@ derive the following property.
 A (possibly mutual) inductive definition is specified by giving the
 names and the type of the inductive sets or families to be
 defined and the names and types of the constructors of the inductive
-predicates.  An inductive declaration in the environment can
-consequently be represented with two contexts (one for inductive
+predicates.  An inductive declaration in the global environment can
+consequently be represented with two local contexts (one for inductive
 definitions, one for constructors).
 
 Stating the rules for inductive definitions in their general form
@@ -574,15 +578,15 @@ forests.
 \subsection{Representing an inductive definition}
 \subsubsection{Inductive definitions without parameters}
 As for constants, inductive definitions can be defined in a non-empty
-context. \\
+local context. \\
 We write \NInd{\Gamma}{\Gamma_I}{\Gamma_C} an inductive
-definition valid in a context $\Gamma$, a
-context of definitions $\Gamma_I$ and a context of constructors
+definition valid in a local context $\Gamma$, a
+context of type definitions $\Gamma_I$ and a context of constructors
 $\Gamma_C$.
 \paragraph{Examples.}
 The inductive declaration for the type of natural numbers will be:
 \[\NInd{}{\nat:\Set}{\nO:\nat,\nS:\nat\ra\nat}\]
-In a context with a variable $A:\Set$, the lists of elements in $A$ are
+In a local context with a variable $A:\Set$, the lists of elements in $A$ are
 represented by:
 \[\NInd{A:\Set}{\List:\Set}{\Nil:\List,\cons : A \ra \List \ra
   \List}\]
@@ -601,7 +605,7 @@ represented by:
 We have to slightly complicate the representation above in order to handle
 the delicate problem of parameters. 
 Let us explain that on the example of \List. With the above definition,
-the type \List\ can only be used in an environment where we
+the type \List\ can only be used in a global environment where we
 have a variable $A:\Set$. Generally one want to consider lists of
 elements in different types. For constants this is easily done by abstracting
 the value over the parameter. In the case of inductive definitions we
@@ -628,11 +632,11 @@ We say that $q$ is the number of real arguments of the constructor
 $c$. 
 \paragraph{Context of parameters.}
 If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits 
-$r$ inductive parameters, then there exists a context $\Gamma_P$ of
+$r$ inductive parameters, then there exists a local context $\Gamma_P$ of
 size $r$, such that $\Gamma_P=[p_1:P_1;\ldots;p_r:P_r]$ and 
 if $(t:A) \in \Gamma_I,\Gamma_C$ then $A$ can be written as 
 $\forall p_1:P_1,\ldots \forall p_r:P_r,A'$. 
-We call $\Gamma_P$ the context of parameters of the inductive
+We call $\Gamma_P$ the local context of parameters of the inductive
 definition and use the notation $\forall \Gamma_P,A'$ for the term $A$.
 \paragraph{Remark.}
 If we have a term $t$ in an instance of an
@@ -660,7 +664,7 @@ But the following definition has $0$ parameters:
 %$\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
 %  \ra (\List~A\ra A) \ra (\List~A)}$.}
 \paragraph{Concrete syntax.}
-In the Coq system, the context of parameters is given explicitly
+In the Coq system, the local context of parameters is given explicitly
 after the name of the inductive definitions and is shared between the
 arities and the type of constructors.
 % The vernacular declaration of polymorphic trees and forests will be:\\
@@ -683,7 +687,7 @@ parameters.
 Formally the representation of an inductive declaration
 will be 
 \Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} for an inductive
-definition valid in a context $\Gamma$ with $p$ parameters, a
+definition valid in a local context $\Gamma$ with $p$ parameters, a
 context of definitions $\Gamma_I$ and a context of constructors
 $\Gamma_C$.
 
@@ -761,7 +765,7 @@ Inductive list' (A:Set) : Set :=
 
 
 \subsection{Types of inductive objects}
-We have to give the type of constants in an environment $E$ which
+We have to give the type of constants in a global environment $E$ which
 contains an inductive declaration.
 
 \begin{description}
@@ -879,7 +883,7 @@ We shall now describe the rules allowing the introduction of a new
 inductive definition.
 
 \begin{description}
-\item[W-Ind] Let $E$ be an environment and
+\item[W-Ind] Let $E$ be a global environment and
   $\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that
   $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall
   \Gamma_P,A_k]$ and $\Gamma_C$ is 
@@ -939,20 +943,21 @@ Inductive exType (P:Type->Prop) : Type
 %a recursive argument and $(x:_P T)C$ if the argument is not recursive.
 
 \paragraph[Sort-polymorphism of inductive families.]{Sort-polymorphism of inductive families.\index{Sort-polymorphism of inductive families}}
+\label{Sort-polymorphism-inductive}
 
 From {\Coq} version 8.1, inductive families declared in {\Type} are
 polymorphic over their arguments in {\Type}.
 
 If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity
 obtained from $A$ by replacing its sort with $s$. Especially, if $A$
-is well-typed in some environment and context, then $A_{/s}$ is typable
+is well-typed in some global environment and local context, then $A_{/s}$ is typable
 by typability of all products in the Calculus of Inductive Constructions.
 The following typing rule is added to the theory.
 
 \begin{description}
 \item[Ind-Family] Let $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ be an
   inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$
-  be its context of parameters, $\Gamma_I = [I_1:\forall
+  be its local context of parameters, $\Gamma_I = [I_1:\forall
     \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of
   definitions and $\Gamma_C = [c_1:\forall
     \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$ its context of
@@ -1103,7 +1108,7 @@ a strongly normalizing reduction, we cannot accept any sort of
 recursion (even terminating). So the basic idea is to restrict
 ourselves to primitive recursive functions and functionals.
 
-For instance, assuming a parameter $A:\Set$ exists in the context, we
+For instance, assuming a parameter $A:\Set$ exists in the local context, we
 want to build a function \length\ of type $\ListA\ra \nat$ which
 computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$
 and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$.  We want these
@@ -1362,7 +1367,7 @@ constructor have type \Prop. In that case, there is a canonical
 way to interpret the informative extraction on an object in that type,
 such that the elimination on any sort $s$ is legal.  Typical examples are
 the conjunction of non-informative propositions and the equality. 
-If there is an hypothesis $h:a=b$ in the context, it can be used for
+If there is an hypothesis $h:a=b$ in the local context, it can be used for
 rewriting not only in logical propositions but also in any type.
 % In that case, the term \verb!eq_rec! which was defined as an axiom, is
 % now a term of the calculus.
@@ -1436,8 +1441,8 @@ only constructors of $I$.
 
 \paragraph{Example.}
 For \List\ and \Length\ the typing rules for the {\tt match} expression
-are (writing just $t:M$ instead of \WTEG{t}{M}, the environment and
-context being the same in all the judgments).
+are (writing just $t:M$ instead of \WTEG{t}{M}, the global environment and
+local context being the same in all the judgments).
 
 \[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~
       f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 80e12898f0..a2be25c3ba 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1250,7 +1250,7 @@ possible, the correct argument will be automatically generated.
 
 \end{ErrMsgs}
 
-\subsection{Declaration of implicit arguments for a constant
+\subsection{Declaration of implicit arguments
 \comindex{Arguments}}
 \label{ImplicitArguments}
 
@@ -1263,7 +1263,7 @@ a priori and a posteriori.
 \subsubsection{Implicit Argument Binders}
 
 In the first setting, one wants to explicitly give the implicit
-arguments of a constant as part of its definition. To do this, one has
+arguments of a declared object as part of its definition. To do this, one has
 to surround the bindings of implicit arguments by curly braces:
 \begin{coq_eval}
 Reset Initial.
@@ -1300,7 +1300,7 @@ usual implicit arguments disambiguation syntax.
 
 \subsubsection{Declaring Implicit Arguments}
 
-To set implicit arguments for a constant a posteriori, one can use the
+To set implicit arguments a posteriori, one can use the
 command:
 \begin{quote}
 \tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
@@ -1379,7 +1379,7 @@ Check (fun l => map length l = map (list nat) nat length l).
 \Rem To know which are the implicit arguments of an object, use the command
 {\tt Print Implicit} (see \ref{PrintImplicit}).
 
-\subsection{Automatic declaration of implicit arguments for a constant}
+\subsection{Automatic declaration of implicit arguments}
 
 {\Coq} can also automatically detect what are the implicit arguments
 of a defined object. The command is just
@@ -1582,7 +1582,7 @@ Implicit arguments names can be redefined using the following syntax:
 \end{quote}
 
 Without the {\tt rename} flag, {\tt Arguments} can be used to assert
-that a given constant has the expected number of arguments and that
+that a given object has the expected number of arguments and that
 these arguments are named as expected.
 
 \noindent {\bf Example (continued): }
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 9b527053c3..e49c82d8fd 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -971,7 +971,7 @@ are the names of its constructors and {\type$_1$}, {\ldots},
 {\type$_n$} their respective types. The types of the constructors have
 to satisfy a {\em positivity condition} (see Section~\ref{Positivity})
 for {\ident}.  This condition ensures the soundness of the inductive
-definition.  If this is the case, the constants {\ident},
+definition.  If this is the case, the names {\ident},
 {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with
 their respective types.  Accordingly to the universe where
 the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a
@@ -990,7 +990,7 @@ Inductive nat : Set :=
 \end{coq_example}
 
 The type {\tt nat} is defined as the least \verb:Set: containing {\tt
-  O} and closed by the {\tt S} constructor. The constants {\tt nat},
+  O} and closed by the {\tt S} constructor. The names {\tt nat},
 {\tt O} and {\tt S} are added to the environment.
 
 Now let us have a look at the elimination principles. They are three
@@ -1101,7 +1101,7 @@ Inductive list (A:Set) : Set :=
 \end{coq_example*}
 
 Note that in the type of {\tt nil} and {\tt cons}, we write {\tt
-  (list A)} and not just {\tt list}.\\ The constants {\tt nil} and
+  (list A)} and not just {\tt list}.\\ The constructors {\tt nil} and
 {\tt cons} will have respectively types:
 
 \begin{coq_example}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b855a0eacc..ddb48b0c1b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1531,25 +1531,27 @@ for each possible form of {\term}, i.e. one for each constructor of
 the inductive or co-inductive type. Unlike {\tt induction}, no
 induction hypothesis is generated by {\tt destruct}.
 
-If the argument is dependent in either the conclusion or some
-hypotheses of the goal, the argument is replaced by the appropriate
-constructor form in each of the resulting subgoals, thus performing
-case analysis. If non-dependent, the tactic simply exposes the
-inductive or co-inductive structure of the argument.
-
 There are special cases:
 
 \begin{itemize}
 
 \item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt destruct {\ident}}
-behaves as {\tt intros until {\ident}; destruct {\ident}}.
+  variable of the conclusion of the goal, then {\tt destruct {\ident}}
+  behaves as {\tt intros until {\ident}; destruct {\ident}}. If
+  {\ident} is not anymore dependent in the goal after application of
+  {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt destruct ({\ident})}).
 
 \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt destruct} applied to the
 last introduced hypothesis. Remark: For destruction of a numeral, use
 syntax {\tt destruct ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt destruct ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1626,14 +1628,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
-\item{\tt destruct !{\ident}}
-
-  This is a case when the destructed term is an hypothesis of the
-  context. The ``!'' modifier tells to keep the hypothesis in the
-  context after destruction.
-
-  This applies also to the other form of {\tt destruct} and {\tt edestruct}.
-
 \item{\tt case \term}\label{case}\tacindex{case}
 
   The tactic {\tt case} is a more basic tactic to perform case
@@ -1699,14 +1693,22 @@ There are particular cases:
 \begin{itemize}
 
 \item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt induction {\ident}}
-behaves as {\tt intros until {\ident}; induction {\ident}}.
+  variable of the conclusion of the goal, then {\tt induction
+    {\ident}} behaves as {\tt intros until {\ident}; induction
+    {\ident}}.  If {\ident} is not anymore dependent in the goal
+  after application of {\tt induction}, it is erased (to avoid
+  erasure, use parentheses, as in {\tt induction ({\ident})}).
 
 \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt induction} applied to the
 last introduced hypothesis. Remark: For simple induction on a numeral,
 use syntax {\tt induction ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt induction}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt induction ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1821,15 +1823,6 @@ Show 2.
   einduction}.  It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:},
   {\tt using}, and {\tt in} clauses.
 
-\item{\tt induction !{\ident}}
-
-  This is a case when the term on which to apply induction is an
-  hypothesis of the context. The ``!'' modifier tells to keep the
-  hypothesis in the context after induction.
-
-  This applies also to the other form of {\tt induction} and {\tt
-    einduction}.
-
 \item {\tt elim \term}\label{elim}
 
   This is a more basic induction tactic.  Again, the type of the
@@ -3562,7 +3555,7 @@ The hints for \texttt{auto} and \texttt{eauto} are stored in
 databases.  Each database maps head symbols to a list of hints. One can
 use the command \texttt{Print Hint \ident} to display the hints
 associated to the head symbol \ident{} (see \ref{PrintHint}). Each
-hint has a cost that is an nonnegative integer, and an optional pattern.
+hint has a cost that is a nonnegative integer, and an optional pattern.
 The hints with lower cost are tried first. A hint is tried by
 \texttt{auto} when the conclusion of the current goal
 matches its pattern or when it has no pattern.
@@ -3779,7 +3772,7 @@ Hint Extern 4 (~(_ = _)) => discriminate.
   with hints with a cost less than 4.
 
   One can even use some sub-patterns of the pattern in the tactic
-  script. A sub-pattern is a question mark followed by an ident, like
+  script. A sub-pattern is a question mark followed by an identifier, like
   \texttt{?X1} or \texttt{?X2}. Here is an example:
 
 % Require EqDecide.
@@ -3822,7 +3815,7 @@ The \texttt{emp} regexp does not match any search path while
 \texttt{eps} matches the empty path. During proof search, the path of
 successive successful hints on a search branch is recorded, as a list of
 identifiers for the hints (note \texttt{Hint Extern}'s do not have an
-associated identitier). Before applying any hint $\ident$ the current
+associated identifier). Before applying any hint $\ident$ the current
 path $p$ extended with $\ident$ is matched against the current cut
 expression $c$ associated to the hint database. If matching succeeds,
 the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$
@@ -4679,7 +4672,7 @@ Use \texttt{classical\_right} to prove the right part of the disjunction with th
 %% procedure for first-order intuitionistic logic implemented in {\em
 %%   NuPRL}\cite{Kre02}.
 
-%% Search may optionnaly be bounded by a multiplicity parameter
+%% Search may optionally be bounded by a multiplicity parameter
 %% indicating how many (at most) copies of a formula may be used in
 %% the proof process, its absence may lead to non-termination of the tactic.