From 410b3cc1cc0f677e052cfedcee03e14521264b64 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 May 2016 17:24:57 +0200
Subject: Program: cleanup in cases, add options

Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
---
 doc/refman/Program.tex | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'doc/refman/Program.tex')

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 11dd3a0517..e07d64cf90 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 global 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{Caseexpr}) when this options 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}
-- 
cgit v1.2.3