From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 doc/refman/Program.tex | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

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

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index b41014ab..96073d71 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -3,11 +3,7 @@
 \aauthor{Matthieu Sozeau}
 \index{Program}
 
-\begin{flushleft}
-  \em The status of \Program\ is experimental.
-\end{flushleft}
-
-We present here the new \Program\ tactic commands, used to build certified
+We present here the \Program\ tactic commands, used to build certified
 \Coq\ programs, elaborating them from their algorithmic skeleton and a
 rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction
 (see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular
@@ -73,6 +69,8 @@ will be first rewrote to:
   works with the previous mechanism.
 \end{itemize}
 
+\subsection{Syntactic control over equalities}
+\label{ProgramSyntax}
 To give more control over the generation of equalities, the typechecker will
 fall back directly to \Coq's usual typing of dependent pattern-matching
 if a {\tt return} or {\tt in} clause is specified. Likewise,
@@ -89,9 +87,18 @@ Program Definition id (n : nat) : { x : nat | x = n } :=
   else S (pred n).
 \end{coq_example}
 
-Finally, the let tupling construct {\tt let (x1, ..., xn) := t in b}
+The let tupling construct {\tt let (x1, ..., xn) := t in b}
 does not produce an equality, contrary to the let pattern construct 
 {\tt let '(x1, ..., xn) := t in b}.
+Also, {\tt {\term}:>} explicitly asks the system to coerce {\tt \term} to its
+support type. It can be useful in notations, for example:
+\begin{coq_example}
+Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing).
+\end{coq_example}
+
+This notation denotes equality on subset types using equality on their
+support types, avoiding uses of proof-irrelevance that would come up
+when reasoning with equality on the subset types themselves. 
 
 The next two commands are similar to their standard counterparts
 Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
-- 
cgit v1.2.3