diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Extraction.tex | 7 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 10 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 16 | ||||
| -rw-r--r-- | doc/refman/RefMan-sch.tex | 7 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 5 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 32 |
6 files changed, 23 insertions, 54 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 01dbcfb1cb..fa3d61b1cd 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -19,6 +19,12 @@ be used (abusively) to refer to any of the three. %% the one in previous versions of \Coq: there is no more %% an explicit toplevel for the language (formerly called \textsc{Fml}). +Before using any of the commands or options described in this chapter, +the extraction framework should first be loaded explicitly +via {\tt Require Extraction}. Note that in earlier versions of Coq, these +commands and options were directly available without any preliminary +{\tt Require}. + \asection{Generating ML code} \comindex{Extraction} \comindex{Recursive Extraction} @@ -501,6 +507,7 @@ We can now extract this program to \ocaml: Reset Initial. \end{coq_eval} \begin{coq_example} +Require Extraction. Require Import Euclid Wf_nat. Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2. Recursive Extraction eucl_dev. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 6dd0ddf81d..939fc87a6e 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -721,18 +721,20 @@ a given type. See Section~\ref{Show}. \section{Advanced recursive functions} -The \emph{experimental} command +The following \emph{experimental} command is available +when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: \begin{center} \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} \{decrease\_annot\} : type$_0$ := \term$_0$} \comindex{Function} \label{Function} \end{center} -can be seen as a generalization of {\tt Fixpoint}. It is actually a -wrapper for several ways of defining a function \emph{and other useful +This command can be seen as a generalization of {\tt Fixpoint}. It is actually +a wrapper for several ways of defining a function \emph{and other useful related objects}, namely: an induction principle that reflects the recursive structure of the function (see \ref{FunInduction}), and its -fixpoint equality. The meaning of this +fixpoint equality. + The meaning of this declaration is to define a function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be given (unless the function is not recursive), but it must not diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 0760d716e3..b66659dc8c 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -427,22 +427,6 @@ This command displays the current goals. This tactics script may contain some holes (subgoals not yet proved). They are printed under the form \verb!<Your Tactic Text here>!. -%% \item {\tt Show Tree.}\comindex{Show Tree}\\ -%% This command can be seen as a more structured way of -%% displaying the state of the proof than that -%% provided by {\tt Show Script}. Instead of just giving -%% the list of tactics that have been applied, it -%% shows the derivation tree constructed by then. -%% Each node of the tree contains the conclusion -%% of the corresponding sub-derivation (i.e. a -%% goal with its corresponding local context) and -%% the tactic that has generated all the -%% sub-derivations. The leaves of this tree are -%% the goals which still remain to be proved. - -%\item {\tt Show Node}\comindex{Show Node}\\ -% Not yet documented - \item {\tt Show Proof.}\comindex{Show Proof}\\ It displays the proof term generated by the tactics that have been applied. diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 53aa6b86ab..d3719bed46 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -196,8 +196,10 @@ Check tree_forest_mutind. 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: +corresponding to (possibly mutually recursive) functions. +First, it must be made available via {\tt Require Import FunInd}. + Its +syntax then follows the schema: \begin{quote} {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ with\\ @@ -319,6 +321,7 @@ of a tree or a forest. Note that we use \texttt{Function} which generally produces better principles. \begin{coq_example*} +Require Import FunInd. Function tree_size (t:tree) : nat := match t with | node A f => S (forest_size f) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 253eb7f01b..2bab04e90a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2113,13 +2113,15 @@ The tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} (see Section~\ref{Function}) or \texttt{Functional Scheme} -(see Section~\ref{FunScheme}). +(see Section~\ref{FunScheme}). Note that this tactic is only available +after a {\tt Require Import FunInd}. \begin{coq_eval} Reset Initial. Import Nat. \end{coq_eval} \begin{coq_example} +Require Import FunInd. Functional Scheme minus_ind := Induction for minus Sort Prop. Check minus_ind. Lemma le_minus (n m:nat) : n - m <= n. @@ -4797,6 +4799,7 @@ that performs inversion on hypothesis {\ident} of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been defined using \texttt{Function} (see Section~\ref{Function}). +Note that this tactic is only available after a {\tt Require Import FunInd}. \begin{ErrMsgs} \item \errindex{Hypothesis {\ident} must contain at least one Function} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index aeb0de48a3..48f82f2d92 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -224,7 +224,6 @@ through the <tt>Require Import</tt> command.</p> <dd> theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v - theories/Numbers/BigNumPrelude.v theories/Numbers/NaryFunctions.v </dd> @@ -256,16 +255,7 @@ through the <tt>Require Import</tt> command.</p> <dd> theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v - theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v + theories/Numbers/Cyclic/Abstract/DoubleType.v theories/Numbers/Cyclic/Int31/Cyclic31.v theories/Numbers/Cyclic/Int31/Ring31.v theories/Numbers/Cyclic/Int31/Int31.v @@ -298,12 +288,6 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v - theories/Numbers/Natural/SpecViaZ/NSig.v - theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v - theories/Numbers/Natural/BigN/BigN.v - theories/Numbers/Natural/BigN/Nbasic.v - theories/Numbers/Natural/BigN/NMake.v - theories/Numbers/Natural/BigN/NMake_gen.v </dd> <dt> <b> Integer</b>: @@ -331,19 +315,6 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/Abstract/ZDivTrunc.v theories/Numbers/Integer/Binary/ZBinary.v theories/Numbers/Integer/NatPairs/ZNatPairs.v - theories/Numbers/Integer/SpecViaZ/ZSig.v - theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v - theories/Numbers/Integer/BigZ/BigZ.v - theories/Numbers/Integer/BigZ/ZMake.v - </dd> - - <dt><b> Rational</b>: - Abstract and 31-bits-words-based rational arithmetic - </dt> - <dd> - theories/Numbers/Rational/SpecViaQ/QSig.v - theories/Numbers/Rational/BigQ/BigQ.v - theories/Numbers/Rational/BigQ/QMake.v </dd> </dl> </dd> @@ -618,7 +589,6 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq84.v theories/Compat/Coq85.v theories/Compat/Coq86.v </dd> |