Fix setoid_rewrite documentation examples.

Debug handling of identifiers in coqdoc (should work with modules and
sections) and add missing macros.
Move theories/Program to THEORIESVO to put the files in the standard
library documentation.


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

1 files changed, 7 insertions, 3 deletions

diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index d2b6d1151..ba847562e 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -623,10 +623,13 @@ Reset Initial.
 Require Import Setoid.
 \end{coq_eval}
 \begin{coq_example}
-Instance {A : Type} => all_iff_morphism : 
+Instance all_iff_morphism (A : Type) :
   Morphism (pointwise_relation iff ==> iff) (@all A).
 Proof. simpl_relation. 
 \end{coq_example}
+\begin{coq_eval}
+Admitted.
+\end{coq_eval}
 
 One then has to show that if two predicates are equivalent at every
 point, their universal quantifications are equivalent. Once we have
@@ -653,12 +656,13 @@ Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) :=
   forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l').
 \end{coq_eval}
 \begin{coq_example*}
-Instance [ Equivalence A eqA, Equivalence B eqB ] => 
+Instance map_morphism [ Equivalence A eqA, Equivalence B eqB ] :
   Morphism ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) 
      (@map A B).
 \end{coq_example*}
 
-where \texttt{list\_equiv} implements an equivalence on lists.
+where \texttt{list\_equiv} implements an equivalence on lists
+parameterized by an equivalence on the elements.
 
 Note that when one does rewriting with a lemma under a binder
 using \texttt{setoid\_rewrite}, the application of the lemma may capture