diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/common/styles/html/coqremote/footer.html | 45 | ||||
| -rw-r--r-- | doc/common/styles/html/coqremote/header.html | 49 | ||||
| -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.html | 13 | ||||
| -rw-r--r-- | doc/refman/RefMan-sch.tex | 418 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 0 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 36 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 34 |
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 |