From 895fcffc774abada4677d52a7dbbb54a85cadec7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 18 Jan 2009 17:36:51 +0000
Subject: 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
---
 doc/refman/Program.tex | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

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

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: 
-- 
cgit v1.2.3