Imported Upstream version 8.4dfsgupstream/8.4dfsg

2 files changed, 6 insertions, 418 deletions

diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
deleted file mode 100644
index 707ee824..00000000
--- a/doc/refman/RefMan-sch.tex
+++ /dev/null
@@ -1,418 +0,0 @@
-\chapter{Proof schemes}
-
-\section{Generation of induction principles with {\tt Scheme}}
-\label{Scheme}
-\index{Schemes}
-\comindex{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:
-\begin{quote}
-{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\\
-        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
-        {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
-identifiers belonging to the same package of mutual inductive
-definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
-to be mutually recursive definitions. Each term {\ident$_i$} proves a
-general principle of mutual induction for objects in type {\term$_i$}.
-
-\begin{Variants}
-\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
-    with\\
-    \mbox{}\hspace{0.1cm} \dots\ \\
-    with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
-    {\sort$_m$}}
-
-  Same as before but defines a non-dependent elimination principle more
-  natural in case of inductively defined relations.
-
-\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
-
-  Tries to generate a boolean equality and a proof of the
-  decidability of the usual equality. If \ident$_i$ involves
-  some other inductive types, their equality has to be defined first.
-
-\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\\
-        with Induction for {\ident$_m$} Sort
-        {\sort$_m$}}
-
-  If you do not provide the name of the schemes, they will be automatically
-  computed from the sorts involved (works also with Minimality).
-
-\end{Variants}
-\label{Scheme-examples}
-
-\firstexample
-\example{Induction scheme for \texttt{tree} and \texttt{forest}}
-
-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}
-Reset Initial.
-Variables A B : Set.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive tree : Set :=
-    node : A -> forest -> tree
-with forest : Set :=
-  | leaf : B -> forest
-  | cons : tree -> forest -> forest.
-
-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 forest\_tree\_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}
-
-\example{Predicates {\tt odd} and {\tt even} on naturals}
-
-Let {\tt odd} and {\tt even} be inductively defined as:
-
-% Reset Initial.
-\begin{coq_eval}
-Open Scope nat_scope.
-\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
-  | 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{Automatic declaration of schemes}
-\comindex{Set Equality Schemes}
-\comindex{Set Elimination Schemes}
-
-It is possible to deactivate the automatic declaration of the induction
- principles when defining a new inductive type  with the
- {\tt Unset Elimination Schemes} command. It may be
-reactivated at any time with {\tt Set Elimination Schemes}.
-\\
-
-You can also activate the automatic declaration of those boolean equalities
-(see the second variant of {\tt Scheme})  with the {\tt Set Equality Schemes}
- command. However you have to be careful with this option since
-\Coq~ may now reject well-defined inductive types because it cannot compute
-a boolean equality for them.
-
-\subsection{\tt Combined Scheme}
-\label{CombinedScheme}
-\comindex{Combined Scheme}
-
-The {\tt Combined Scheme} command is a tool for combining
-induction principles generated by the {\tt Scheme} command.
-Its syntax follows the schema :
-\begin{quote}
-{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}
-\end{quote}
-where
-\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
-built from the common premises of the principles and concluded by the
-conjunction of their conclusions.
-
-\Example
-We can define the induction principles for trees and forests using:
-\begin{coq_example}
-Scheme tree_forest_ind := Induction for tree Sort Prop
-  with forest_tree_ind := Induction for forest Sort Prop.
-\end{coq_example}
-
-Then we can build the combined induction principle which gives the
-conjunction of the conclusions of each individual principle:
-\begin{coq_example}
-Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
-\end{coq_example}
-
-The type of {\tt tree\_forest\_mutrec} will be:
-\begin{coq_example}
-Check tree_forest_mutind.
-\end{coq_example}
-
-\section{Generation of induction principles with {\tt Functional Scheme}}
-\label{FunScheme}
-\comindex{Functional Scheme}
-
-The {\tt Functional Scheme} command is a high-level experimental
-tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions.  Its
-syntax follows the schema:
-\begin{quote}
-{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\ \\
-        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
-        {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
-names (they must be in the same order as when they were defined).
-This command generates the induction principles
-\ident$_1$\dots\ident$_m$, following the recursive structure and case
-analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
-
-\Rem
-There is a difference between obtaining an induction scheme by using
-\texttt{Functional Scheme} on a function defined by \texttt{Function}
-or not. Indeed \texttt{Function} generally produces smaller
-principles, closer to the definition written by the user.
-
-\firstexample
-\example{Induction scheme for \texttt{div2}}
-\label{FunScheme-examples}
-
-We define the function \texttt{div2} as follows:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Require Import Arith.
-Fixpoint div2 (n:nat) : nat :=
-  match n with
-  | O => 0
-  | S O => 0
-  | S (S n') => S (div2 n')
-  end.
-\end{coq_example*}
-
-The definition of a principle of induction corresponding to the
-recursive structure of \texttt{div2} is defined by the command:
-
-\begin{coq_example}
-Functional Scheme div2_ind := Induction for div2 Sort Prop.
-\end{coq_example}
-
-You may now look at the type of {\tt div2\_ind}:
-
-\begin{coq_example}
-Check div2_ind.
-\end{coq_example}
-
-We can now prove the following lemma using this principle:
-
-\begin{coq_example*}
-Lemma div2_le' : forall n:nat, div2 n <= n.
-intro n.
- pattern n , (div2 n).
-\end{coq_example*}
-
-\begin{coq_example}
-apply div2_ind; intros.
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-simpl; auto with arith.
-Qed.
-\end{coq_example*}
-
-We can use directly the \texttt{functional induction}
-(\ref{FunInduction}) tactic instead of the pattern/apply trick:
-\tacindex{functional induction}
-
-\begin{coq_example*}
-Reset div2_le'.
-Lemma div2_le : forall n:nat, div2 n <= n.
-intro n.
-\end{coq_example*}
-
-\begin{coq_example}
-functional induction (div2 n).
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-auto with arith.
-Qed.
-\end{coq_example*}
-
-\Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (see Section~\ref{Function}) and by
-using \texttt{Functional Scheme} after a normal definition using
-\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
-details.
-
-
-\example{Induction scheme for \texttt{tree\_size}}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-We define trees by the following mutual inductive type:
-
-\begin{coq_example*}
-Variable A : Set.
-Inductive tree : Set :=
-    node : A -> forest -> tree
-with forest : Set :=
-  | empty : forest
-  | cons : tree -> forest -> forest.
-\end{coq_example*}
-
-We define the function \texttt{tree\_size} that computes the size
-of a tree or a forest. Note that we use \texttt{Function} which
-generally produces better principles.
-
-\begin{coq_example*}
-Function tree_size (t:tree) : nat :=
-  match t with
-  | node A f => S (forest_size f)
-  end
- with forest_size (f:forest) : nat :=
-  match f with
-  | empty => 0
-  | cons t f' => (tree_size t + forest_size f')
-  end.
-\end{coq_example*}
-
-\Rem \texttt{Function} generates itself non mutual induction
-principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
-
-\begin{coq_example}
-Check tree_size_ind.
-\end{coq_example}
-
-The definition of mutual induction principles following the recursive
-structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
-by the command:
-
-\begin{coq_example*}
-Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
-with forest_size_ind2 := Induction for forest_size Sort Prop.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_size\_ind2}:
-
-\begin{coq_example}
-Check tree_size_ind2.
-\end{coq_example}
-
-\section{Generation of inversion principles with \tt Derive Inversion}
-\label{Derive-Inversion}
-\comindex{Derive Inversion}
-
-The syntax of {\tt Derive Inversion} follows the schema:
-\begin{quote}
-{\tt Derive Inversion {\ident} with forall
-  $(\vec{x} : \vec{T})$, $I~\vec{t}$ Sort \sort}
-\end{quote}
-
-This command generates an inversion principle for the
-\texttt{inversion \dots\ using} tactic.
-\tacindex{inversion \dots\ using}
-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
-$\forall (\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 {\tt inversion}.
-
-\begin{Variants}
-\item \texttt{Derive Inversion\_clear {\ident} with forall
-  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
-  \comindex{Derive Inversion\_clear}
-  When applied, it is equivalent to having
-  inverted the instance with the tactic \texttt{inversion}
-  replaced by the tactic \texttt{inversion\_clear}.
-\item \texttt{Derive Dependent Inversion {\ident} with forall
-  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
-  \comindex{Derive Dependent Inversion}
-  When applied, it is equivalent to having
-  inverted the instance with the tactic \texttt{dependent inversion}.
-\item \texttt{Derive Dependent Inversion\_clear {\ident} with forall
-  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
-  \comindex{Derive Dependent Inversion\_clear}
-  When applied, it is equivalent to having
-  inverted the instance with the tactic \texttt{dependent inversion\_clear}.
-\end{Variants}
-
-\Example
-
-Let us consider the relation \texttt{Le} over natural numbers and the
-following variable:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive Le : nat -> nat -> Set :=
-  | LeO : forall n:nat, Le 0 n
-  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-Variable P : nat -> nat -> Prop.
-\end{coq_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*}
-
-\begin{coq_example}
-Check leminv.
-\end{coq_example}
-
-Then we can use the proven inversion lemma:
-
-\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}
-
-\begin{coq_example}
-inversion H using leminv.
-\end{coq_example}
-
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0ee101c8..833b5c4c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -400,6 +400,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Lists/List.v
     theories/Lists/ListSet.v
     theories/Lists/SetoidList.v
+    theories/Lists/SetoidPermutation.v
     theories/Lists/Streams.v
     theories/Lists/StreamMemo.v
     theories/Lists/ListTactics.v
@@ -523,7 +524,10 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/Rsigma.v
     theories/Reals/R_sqr.v
     theories/Reals/Rtrigo_fun.v
+    theories/Reals/Rtrigo1.v
     theories/Reals/Rtrigo.v
+    theories/Reals/Ratan.v
+    theories/Reals/Machin.v
     theories/Reals/SplitAbsolu.v
     theories/Reals/SplitRmult.v
     theories/Reals/Alembert.v
@@ -544,6 +548,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/Ranalysis2.v
     theories/Reals/Ranalysis3.v
     theories/Reals/Ranalysis4.v
+    theories/Reals/Ranalysis5.v
+    theories/Reals/Ranalysis_reg.v
     theories/Reals/Rcomplete.v
     theories/Reals/RiemannInt.v
     theories/Reals/RiemannInt_SF.v