diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 3a99bfdd4f..2fc1c8764a 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -63,10 +63,27 @@ will be first rewritten to: previous one, an inequality is added in the context of the second branch. See for example the definition of {\tt div2} below, where the second branch is typed in a context where $\forall p, \_ <> S (S p)$. - + \item Coercion. If the object being matched is coercible to an inductive type, the corresponding coercion will be automatically inserted. This also works with the previous mechanism. + +\end{itemize} + +There are options to control the generation of equalities +and coercions. + +\begin{itemize} +\item {\tt Unset Program Cases}\optindex{Program Cases} This deactivates + the special treatment of pattern-matching generating equalities and + inequalities when using \Program\ (it is on by default). All + pattern-matchings and let-patterns are handled using the standard + algorithm of Coq (see Section~\ref{Mult-match-full}) when this option is + deactivated. +\item {\tt Unset Program Generalized Coercion}\optindex{Program + Generalized Coercion} This deactivates the coercion of general + inductive types when using \Program\ (the option is on by default). + Coercion of subset types and pairs is still active in this case. \end{itemize} \subsection{Syntactic control over equalities} @@ -261,7 +278,7 @@ tactic is replaced by the default one if not specified. as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} - Control whether obligations defined by tactics should have their + Control whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. \end{itemize} |