Last changes in type class syntax:

- curly braces mandatory for record class instances
- no mention of the unique method for definitional class instances
Turning a record or definition into a class is mostly a 
matter of changing the keywords to 'Class' and 'Instance' now.
Documentation reflects these changes, and was checked once more 
along with setoid_rewrite's and Program's.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11797 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 5 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index dfcebf1860..20444dc0a1 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -137,18 +137,18 @@ Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
 \end{coq_example}
 
 Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are
-automatically generated by the pattern-matching compilation algorithm):
+automatically generated by the pattern-matching compilation algorithm).
 \begin{coq_example}
-  Obligations.
+  Obligation 1.
 \end{coq_example}
 
-You can use a well-founded order or a measure as termination orders using the syntax:
+One can use a well-founded order or a measure as termination orders using the syntax:
 \begin{coq_eval}
 Reset Initial.
 Require Import Arith.
 Require Import Program.
 \end{coq_eval}
-\begin{coq_example}
+\begin{coq_example*}
 Definition id (n : nat) := n.
 Program Fixpoint div2 (n : nat) {measure id n} :
   { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
@@ -156,7 +156,7 @@ Program Fixpoint div2 (n : nat) {measure id n} :
   | S (S p) => S (div2 p)
   | _ => O
   end.
-\end{coq_example}
+\end{coq_example*}
 
 The \verb|measure| keyword expects a measure function into the naturals, whereas
 \verb|wf| expects a relation.
@@ -270,4 +270,5 @@ Program Fixpoint f (x : A | P) { measure size } :=
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
+%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
 %%% End: