diff options
Diffstat (limited to 'doc')
-rw-r--r-- | doc/faq/FAQ.tex | 2 | ||||
-rw-r--r-- | doc/refman/Extraction.tex | 4 | ||||
-rw-r--r-- | doc/refman/Helm.tex | 2 | ||||
-rw-r--r-- | doc/refman/Polynom.tex | 12 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-tacex.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-tus.tex | 3 |
7 files changed, 13 insertions, 14 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 4309926b9..baf3d4991 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1983,7 +1983,7 @@ todo \Question{Can you show me an example of a tactic written in OCaml?} -You have some examples of tactics written in Ocaml in the ``contrib'' directory of {\Coq} sources. +You have some examples of tactics written in Ocaml in the ``plugins'' directory of {\Coq} sources. diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index ba07182a6..8271c7c32 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -620,7 +620,7 @@ quite efficient for Caml code. As a test, we propose an automatic extraction of the Standard Library of \Coq. In particular, we will find back the two previous examples, {\tt Euclid} and {\tt Heapsort}. -Go to directory {\tt contrib/extraction/test} of the sources of \Coq, +Go to directory {\tt plugins/extraction/test} of the sources of \Coq, and run commands: \begin{verbatim} make tree; make @@ -653,7 +653,7 @@ also work, just adapt the {\tt Makefile.haskell}. In particular {\tt Some pathological examples of extraction are grouped in the file \begin{verbatim} -contrib/extraction/test_extraction.v +plugins/extraction/test_extraction.v \end{verbatim} of the sources of \Coq. diff --git a/doc/refman/Helm.tex b/doc/refman/Helm.tex index d07b1204c..74db9c86d 100644 --- a/doc/refman/Helm.tex +++ b/doc/refman/Helm.tex @@ -273,7 +273,7 @@ of the calculus is also proved. \subsubsection{The CIC with Explicit Named Substitutions XML DTD} A copy of the DTD can be found in the file ``\verb+cic.dtd+'' in the -\verb+contrib/xml+ source directory of \Coq. +\verb+plugins/xml+ source directory of \Coq. The following is a very brief overview of the elements described in the DTD. \begin{description} diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 48937113f..94c76c197 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -336,21 +336,21 @@ describes their syntax and effects: evaluation function of power coefficient) is the original term, or returns {\tt InitialRing.NotConstant} if not a constant coefficient (i.e. {\ltac} is the inverse function of {\tt Cp\_phi}). - See files {\tt contrib/setoid\_ring/ZArithRing.v} and - {\tt contrib/setoid\_ring/RealField.v} for examples. + See files {\tt plugins/setoid\_ring/ZArithRing.v} and + {\tt plugins/setoid\_ring/RealField.v} for examples. By default the tactic does not recognize power expressions as ring expressions. \item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$. The term {\term} is a proof that a given sign function indicates expressions that are signed ({\term} has to be a - proof of {\tt Ring\_theory.get\_sign}). See {\tt contrib/setoid\_ring/IntialRing.v} for examples of sign function. + proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function. \item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use moniomals with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function satisfies the specification of an euclidean division function ({\term} has to be a proof of {\tt Ring\_theory.div\_theory}). For example, this function is called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$. - See {\tt contrib/setoid\_ring/IntialRing.v} for examples of div function. + See {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function. \end{description} @@ -490,7 +490,7 @@ constants can be proven different from zero automatically. The tactic must be loaded by \texttt{Require Import Field}. New field structures can be declared to the system with the \texttt{Add Field} command (see below). The field of real numbers is defined in module -\texttt{RealField} (in texttt{contrib/setoid\_ring}). It is exported +\texttt{RealField} (in texttt{plugins/setoid\_ring}). It is exported by module \texttt{Rbase}, so that requiring \texttt{Rbase} or \texttt{Reals} is enough to use the field tactics on real numbers. Rational numbers in canonical form are also declared as a @@ -696,7 +696,7 @@ the file \begin{quotation} \begin{verbatim} -contrib/ring/Ring_theory.v +plugins/ring/Ring_theory.v \end{verbatim} \end{quotation} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9ed2e650c..4e31137c9 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3565,7 +3565,7 @@ intros; field. Reset Initial. \end{coq_eval} -\SeeAlso file {\tt contrib/setoid\_ring/RealField.v} for an example of instantiation,\\ +\SeeAlso file {\tt plugins/setoid\_ring/RealField.v} for an example of instantiation,\\ \phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt field}. diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index dbd863469..9af44115a 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -1084,7 +1084,7 @@ is undecidable in general case, don't expect miracles from it! % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} -\SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml} +\SeeAlso comments of source file \texttt{plugins/quote/quote.ml} \SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring}) diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index d7239c8fd..5a3ccda6a 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -1186,8 +1186,7 @@ function body or behind the \texttt{lazy} keyword. One can see examples of that technique in the source code of \Coq{}, for example -\verb+tactics/contrib/polynom/ring.ml+ or -\verb+tactics/contrib/polynom/coq_omega.ml+. +\verb+plugins/omega/coq_omega.ml+. \section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}} When the implementation of a tactic is not a straightforward |