summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/common/styles/html/coqremote/footer.html45
-rw-r--r--doc/common/styles/html/coqremote/header.html49
-rw-r--r--doc/common/styles/html/simple/footer.html (renamed from doc/stdlib/index-trailer.html)0
-rw-r--r--doc/common/styles/html/simple/header.html13
-rw-r--r--doc/refman/RefMan-sch.tex418
-rw-r--r--doc/stdlib/hidden-files0
-rw-r--r--doc/stdlib/index-list.html.template36
-rwxr-xr-xdoc/stdlib/make-library-index34
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