diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Cases.tex | 12 | ||||
| -rw-r--r-- | doc/refman/Classes.tex | 4 | ||||
| -rw-r--r-- | doc/refman/Omega.tex | 26 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 54 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 17 | ||||
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-sch.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 48 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 55 |
10 files changed, 168 insertions, 62 deletions
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 7ad895f9d8..376ef031db 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -280,6 +280,18 @@ Fail Check end). \end{coq_example} +The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns} +(off by default) removes parameters from constructors in patterns: +\begin{coq_example} + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end) + Unset Asymmetric Patterns. +\end{coq_example} + \paragraph{Implicit arguments in patterns} By default, implicit arguments are omitted in patterns. So we write: diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index cab6739998..6e76d04e77 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -526,14 +526,14 @@ potentially more expensive proof-search (i.e. more useless backtracking). \subsection{\tt Set Typeclass Resolution After Apply} -\optindex{Typeclasses Resolution After Apply} +\optindex{Typeclass Resolution After Apply} \emph{Deprecated since 8.6} This option (off by default in Coq 8.6 and 8.5) controls the resolution of typeclass subgoals generated by the {\tt apply} tactic. \subsection{\tt Set Typeclass Resolution For Conversion} -\optindex{Typeclasses Resolution For Conversion} +\optindex{Typeclass Resolution For Conversion} This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex index 8025fbe29f..82765da6ed 100644 --- a/doc/refman/Omega.tex +++ b/doc/refman/Omega.tex @@ -149,6 +149,32 @@ intro; omega. % Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. +\section{Options} + +\begin{quote} + \optindex{Stable Omega} + {\tt Unset Stable Omega} +\end{quote} +This deprecated option (on by default) is for compatibility with Coq +pre 8.5. It resets internal name counters to make executions of +{\tt omega} independent. + +\begin{quote} + \optindex{Omega UseLocalDefs} + {\tt Unset Omega UseLocalDefs} +\end{quote} +This option (on by default) allows {\tt omega} to use the bodies of +local variables. + +\begin{quote} + \optindex{Omega System} + {\tt Set Omega System} + \optindex{Omega Action} + {\tt Set Omega Action} +\end{quote} +These two options (off by default) activate the printing of debug +information. + \asection{Technical data} \label{technical} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 5c519e46e3..a1950d136e 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -550,6 +550,60 @@ the same way as the {\Coq} kernel handles them. This tells if the printing matching mode is on or off. The default is on. +\subsubsection{Factorization of clauses with same right-hand side} +\label{SetPrintingFactorizableMatchPatterns} +\optindex{Printing Factorizable Match Patterns} + +When several patterns share the same right-hand side, it is +additionally possible to share the clauses using disjunctive patterns. +Assuming that the printing matching mode is on, whether {\Coq}'s +printer shall try to do this kind of factorization is governed by the +following commands: + +\begin{quote} +{\tt Set Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer not to try to use disjunctive patterns. + +\begin{quote} +{\tt Test Printing Factorizable Match Patterns.} +\end{quote} +This tells if the factorization of clauses with same right-hand side is +on or off. + +\subsubsection{Use of a default clause} +\label{SetPrintingAllowDefaultClause} +\optindex{Printing Allow Default Clause} + +When several patterns share the same right-hand side which do not +depend on the arguments of the patterns, yet an extra factorization is +possible: the disjunction of patterns can be replaced with a ``{\tt + \_}'' default clause. Assuming that the printing matching mode and +the factorization mode are on, whether {\Coq}'s printer shall try to +use a default clause is governed by the following commands: + +\begin{quote} +{\tt Set Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer to use a default clause when relevant. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer not to use a default clause. + +\begin{quote} +{\tt Test Printing Allow Default Clause.} +\end{quote} +This tells if the use of a default clause is allowed. + \subsubsection{Printing of wildcard pattern \optindex{Printing Wildcard}} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 7034c56081..8d82460a72 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -198,8 +198,6 @@ is understood as {\cpattern} {\tt =>} {\tacexpr}\\ & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\ -& $|$ & {\tt appcontext} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} - {\tt =>} {\tacexpr}\\ & $|$ & {\tt \_ =>} {\tacexpr}\\ \\ {\it test} & ::= & @@ -876,21 +874,6 @@ Goal True. f (3+4). \end{coq_example} -\item \index{appcontext@\texttt{appcontext}!in pattern} - \optindex{Tactic Compat Context} -For historical reasons, {\tt context} used to consider $n$-ary applications -such as {\tt (f 1 2)} as a whole, and not as a sequence of unary -applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail -to find a matching subterm in {\tt (f 1 2)}: if the pattern was a partial -application, the matched subterms would have necessarily been -applications with exactly the same number of arguments. -As a workaround, one could use the following variant of {\tt context}: -\begin{quote} -{\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]} -\end{quote} -This syntax is now deprecated, as {\tt context} behaves as intended. The former -behavior can be retrieved with the {\tt Tactic Compat Context} flag. - \end{Variants} \subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal} diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index e56c8fa7fe..b4e270e6c3 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -403,10 +403,14 @@ Fail Check B.T. \end{Warnings} \subsection{\tt Print Module {\ident} -\comindex{Print Module}} +\comindex{Print Module} \optindex{Short Module Printing}} Prints the module type and (optionally) the body of the module {\ident}. +For this command and {\tt Print Module Type}, the option {\tt Short + Module Printing} (off by default) disables the printing of the types of fields, +leaving only their names. + \subsection{\tt Print Module Type {\ident} \comindex{Print Module Type}} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 8f659ded35..1d3311edc2 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -395,6 +395,8 @@ Proof. \end{ErrMsgs} +\subsection[\tt Set Bullet Behavior.]{\tt Set Bullet Behavior.\optindex{Bullet Behavior}} + The bullet behavior can be controlled by the following commands. \begin{quote} diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 956f308512..30724759d2 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -127,8 +127,10 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} +\optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} +\optindex{Rewriting Schemes} \label{set-nonrecursive-elimination-schemes} } @@ -142,6 +144,7 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. +{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}. In addition, the {\tt Case Analysis Schemes} flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the @@ -156,6 +159,9 @@ 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. +The {\tt Rewriting Schemes} flag governs generation of equality +related schemes such as congruence. + \subsection{\tt Combined Scheme} \label{CombinedScheme} \comindex{Combined Scheme} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 675c2bf174..66a5f107a5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3334,6 +3334,14 @@ evaluating purely computational expressions (i.e. with little dead code). \end{Variants} +\Rem The following option makes {\tt cbv} (and its derivative {\tt + compute}) print information about the constants it encounters and +the unfolding decisions it makes. +\begin{quote} + \optindex{Debug Cbv} + {\tt Set Debug Cbv} +\end{quote} + % Obsolete? Anyway not very important message %\begin{ErrMsgs} %\item \errindex{Delta must be specified before} @@ -3507,6 +3515,13 @@ of {\tt cbn} while doing reductions in unification, type inference and tactic applications. It can result in expensive unifications, as refolding currently uses a potentially exponential heuristic. +\begin{quote} + \optindex{Debug RAKAM} + {\tt Set Debug RAKAM} +\end{quote} +This option makes {\tt cbn} print various debugging information. +{\tt RAKAM} is the Refolding Algebraic Krivine Abstract Machine. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} @@ -3703,6 +3718,9 @@ hints of the database named {\tt core}. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. +\item {\tt debug auto} Behaves like {\tt auto} but shows the tactics + it tries to solve the goal, including failing paths. + \item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3723,6 +3741,8 @@ hints of the database named {\tt core}. \item {\tt info\_trivial} +\item {\tt debug trivial} + \item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3732,6 +3752,19 @@ hints of the database named {\tt core}. \Rem {\tt auto} either solves completely the goal or else leaves it intact. \texttt{auto} and \texttt{trivial} never fail. +\Rem The following options enable printing of informative or debug +information for the {\tt auto} and {\tt trivial} tactics: +\begin{quote} + \optindex{Info Auto} + {\tt Set Info Auto} + \optindex{Debug Auto} + {\tt Set Debug Auto} + \optindex{Info Trivial} + {\tt Set Info Trivial} + \optindex{Debug Trivial} + {\tt Set Debug Trivial} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt eauto} @@ -3768,6 +3801,14 @@ Note that {\tt ex\_intro} should be declared as a hint. \end{Variants} +\Rem {\tt eauto} obeys the following options: +\begin{quote} + \optindex{Info Eauto} + {\tt Set Info Eauto} + \optindex{Debug Eauto} + {\tt Set Debug Eauto} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$} @@ -4710,6 +4751,13 @@ congruence. described above. \end{ErrMsgs} +\noindent {\bf Remark: } {\tt congruence} can be made to print debug +information by setting the following option: + +\begin{quote} +\optindex{Congruence Verbose} +{\tt Set Congruence Verbose} +\end{quote} \section{Checking properties of terms} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index c411db1001..962aa98b68 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -4,53 +4,24 @@ The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}} +\section[Using Coq as a library]{Using Coq as a library} -The native-code version of \Coq\ cannot dynamically load user tactics -using {\ocaml} code. It is possible to build a toplevel of \Coq, -with {\ocaml} code statically linked, with the tool {\tt - coqmktop}. - -For example, one can build a native-code \Coq\ toplevel extended with a tactic -which source is in {\tt tactic.ml} with the command -\begin{verbatim} - % coqmktop -opt -o mytop.out tactic.cmx -\end{verbatim} -where {\tt tactic.ml} has been compiled with the native-code -compiler {\tt ocamlopt}. This command generates an executable -called {\tt mytop.out}. To use this executable to compile your \Coq\ -files, use {\tt coqc -image mytop.out}. - -A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}), -which can be generated by {\tt coqmktop -opt -o coqopt.opt}. - - -\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}} - -One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in -order to debug your tactics with the {\ocaml} debugger. -You need to have configured and compiled \Coq\ for debugging -(see the file \texttt{INSTALL} included in the distribution). -Then, you must compile the Caml modules of your tactic with the -option \texttt{-g} (with the bytecode compiler) and build a stand-alone -bytecode toplevel with the following command: +In previous versions, \texttt{coqmktop} was used to build custom +toplevels --- for example for better debugging or custom static +linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. +The most basic custom toplevel is built using: \begin{quotation} -\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} - -To launch the \ocaml\ debugger with the image you need to execute it in -an environment which correctly sets the \texttt{COQLIB} variable. -Moreover, you have to indicate the directories in which -\texttt{ocamldebug} should search for Caml modules. - -A possible solution is to use a wrapper around \texttt{ocamldebug} -which detects the executables containing the word \texttt{coq}. In -this case, the debugger is called with the required additional -arguments. In other cases, the debugger is simply called without additional -arguments. Such a wrapper can be found in the \texttt{dev/} -subdirectory of the sources. +For example, to statically link LTAC, you can just do: +\begin{quotation} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native} +\end{quotation} +and similarly for other plugins. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |