Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg

author: Stephane Glondu <steph@glondu.net> 2012-06-04 12:23:14 +0200
committer: Stephane Glondu <steph@glondu.net> 2012-06-04 12:23:14 +0200
commit: 86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree: 9b221c283c2971f7ac151397231059e1d239e723 /doc
parent: 39efc41237ec906226a3a53d7396d51173495204 (diff)
parent: 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
8 files changed, 574 insertions, 21 deletions
diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html
new file mode 100644
index 00000000..138c3025
--- /dev/null
+++ b/doc/common/styles/html/coqremote/footer.html
@@ -0,0 +1,45 @@
+<div id="sidebarWrapper">
+<div id="sidebar">
+
+<div class="block">
+<h2 class="title">Navigation</h2>
+<div class="content">
+
+<ul class="menu">
+
+<li class="leaf">Standard Library
+  <ul class="menu">
+  <li><a href="index.html">Table of contents</a></li>
+  <li><a href="genindex.html">Index</a></li>
+  </ul>
+</li>
+
+</ul>
+
+</div>
+</div>
+
+</div>
+</div>
+
+
+</div>
+
+</div>
+
+<div id="footer">
+<div id="nav-footer">
+  <ul class="links-menu-footer">
+    <li><a href="mailto:webmaster_@_www.lix.polytechnique.fr">webmaster</a></li>
+    <li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li>
+    <li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li>
+  </ul>
+
+</div>
+</div>
+
+</div>
+
+</body>
+</html>
+
diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html
new file mode 100644
index 00000000..afcdbe73
--- /dev/null
+++ b/doc/common/styles/html/coqremote/header.html
@@ -0,0 +1,49 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
+<title>Standard Library | The Coq Proof Assistant</title>
+
+<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" />
+<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/node/node.css";</style>
+
+<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/system/defaults.css";</style>
+<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/system/system.css";</style>
+<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/user/user.css";</style>
+
+<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/sites/all/themes/coq/style.css";</style>
+<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/sites/all/themes/coq/coqdoc.css";</style>
+
+</head>
+
+<body>
+
+<div id="container">
+<div id="headertop">
+<div id="nav">
+  <ul class="links-menu">
+    <li><a href="http://www.lix.polytechnique.fr/coq/" class="active">Home</a></li>
+
+    <li><a href="http://www.lix.polytechnique.fr/coq/about-coq" title="More about coq">About Coq</a></li>    
+    <li><a href="http://www.lix.polytechnique.fr/coq/download">Get Coq</a></li>
+    <li><a href="http://www.lix.polytechnique.fr/coq/documentation">Documentation</a></li>
+    <li><a href="http://www.lix.polytechnique.fr/coq/community">Community</a></li>
+  </ul>
+</div>
+</div>
+
+<div id="header">
+
+<div id="logoWrapper">
+
+<div id="logo"><a href="http://www.lix.polytechnique.fr/coq/" title="Home"><img src="http://www.lix.polytechnique.fr/coq/files/barron_logo.png" alt="Home" /></a>
+</div>
+<div id="siteName"><a href="http://www.lix.polytechnique.fr/coq/" title="Home">The Coq Proof Assistant</a>
+</div>
+
+</div>
+</div>
+
+<div id="content">
+
diff --git a/doc/stdlib/index-trailer.html b/doc/common/styles/html/simple/footer.html
index 308b1d01..308b1d01 100644
--- a/doc/stdlib/index-trailer.html
+++ b/doc/common/styles/html/simple/footer.html
diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html
new file mode 100644
index 00000000..14d2f988
--- /dev/null
+++ b/doc/common/styles/html/simple/header.html
@@ -0,0 +1,13 @@
+<!DOCTYPE html 
+     PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+
+<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
+<link rel="stylesheet" href="coqdoc.css" type="text/css"/>
+<title>The Coq Standard Library</title>
+</head>
+
+<body>
+
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
new file mode 100644
index 00000000..707ee824
--- /dev/null
+++ b/doc/refman/RefMan-sch.tex
@@ -0,0 +1,418 @@
+\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/hidden-files b/doc/stdlib/hidden-files
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/doc/stdlib/hidden-files
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 35c13f3b..0ee101c8 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -1,17 +1,5 @@
-<!DOCTYPE html 
-     PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
-    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
 
-<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
-<head>
-<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
-<link rel="stylesheet" href="css/context.css" type="text/css"/>
-<title>The Coq Standard Library</title>
-</head>
-
-<body>
-
-<H1>The Coq Standard Library</H1>
+<h1>The Coq Standard Library</h1>
 
 <p>Here is a short description of the Coq standard library, which is
 distributed with the system.
@@ -68,6 +56,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
     theories/Logic/FunctionalExtensionality.v
+    theories/Logic/ExtensionalityFacts.v
   </dd>
     
   <dt> <b>Structures</b>:
@@ -184,6 +173,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/ZArith/Zpow_def.v
     theories/ZArith/Zpow_alt.v
     theories/ZArith/Zpower.v
+    theories/ZArith/ZOdiv_def.v
+    theories/ZArith/ZOdiv.v
     theories/ZArith/Zdiv.v
     theories/ZArith/Zquot.v
     theories/ZArith/Zeuclid.v
@@ -414,6 +405,16 @@ through the <tt>Require Import</tt> command.</p>
     theories/Lists/ListTactics.v
   </dd>
 
+  <dt> <b>Vectors</b>:
+    Dependent datastructures storing their length
+  </dt>
+  <dd>
+    theories/Vectors/Fin.v
+    theories/Vectors/VectorDef.v
+    theories/Vectors/VectorSpec.v
+    (theories/Vectors/Vector.v)
+  </dd>
+
   <dt> <b>Sorting</b>:
     Axiomatizations of sorts
   </dt>
@@ -454,7 +455,9 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetEqProperties.v
     theories/MSets/MSetWeakList.v
     theories/MSets/MSetList.v
+    theories/MSets/MSetGenTree.v
     theories/MSets/MSetAVL.v
+    theories/MSets/MSetRBT.v
     theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.v)
@@ -576,4 +579,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Program/Combinators.v
   </dd>
 
+  <dt> <b>Unicode</b>:
+    Unicode-based notations
+  </dt>
+  <dd>
+    theories/Unicode/Utf8_core.v
+    theories/Unicode/Utf8.v
+  </dd>
 </dl>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 8e496fdd..1a70567f 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -3,37 +3,55 @@
 # Instantiate links to library files in index template
 
 FILE=$1
+HIDDEN=$2
 
 cp -f $FILE.template tmp
 echo -n Building file index-list.prehtml ...
 
-LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
+#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
+LIBDIRS=`find theories/* -type d | sed -e "s:^theories/::"`
 
 for k in $LIBDIRS; do
     i=theories/$k
     echo $i
     
     d=`basename $i`
-    if [ "$d" != "Num" -a "$d" != "CVS" ]; then
+    if [ "$d" != "CVS" ]; then
+      ls $i | grep -q \.v'$'
+      if [ $? = 0 ]; then
 	for j in $i/*.v; do
 	    b=`basename $j .v`
 	    rm -f tmp2
 	    grep -q theories/$k/$b.v tmp
 	    a=$?
+	    grep -q theories/$k/$b.v $HIDDEN
+	    h=$?
 	    if [ $a = 0 ]; then
-		p=`echo $k | sed 's:/:.:g'`
-		sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
-		mv -f tmp2 tmp
+	        if [ $h = 0 ]; then
+                    echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1
+                else
+		    p=`echo $k | sed 's:/:.:g'`
+		    sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+		    mv -f tmp2 tmp
+                fi
 	    else
-		echo Warning: theories/$k/$b.v is missing in the template file
-	    fi
+	        if [ $h = 0 ]; then
+		    echo Error: theories/$k/$b.v is missing in the template file
+                    exit 1
+                else
+                    echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v
+                    exit 1
+	        fi
+
+            fi
 	done
+      fi
     fi
     rm -f tmp2
     sed -e "s/#$d#//" tmp > tmp2
     mv -f tmp2 tmp
 done
 a=`grep theories tmp`
-if [ $? = 0 ]; then echo Warning: extra files:; echo $a; fi
+if [ $? = 0 ]; then echo Error: extra files:; echo $a; exit 1; fi
 mv tmp $FILE
 echo Done
author	Stephane Glondu <steph@glondu.net>	2012-06-04 12:23:14 +0200
committer	Stephane Glondu <steph@glondu.net>	2012-06-04 12:23:14 +0200
commit	86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree	9b221c283c2971f7ac151397231059e1d239e723 /doc
parent	39efc41237ec906226a3a53d7396d51173495204 (diff)
parent	61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)