documentation automatique de la bibliothèque standard

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

1 files changed, 4 insertions, 2 deletions

diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 08a054900..35a25a46f 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -99,11 +99,13 @@ Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
 
-(*** not allowed because of dependencies 
+(* not allowed because of dependencies:
+\begin{verbatim}
 Definition eqT_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)y==x -> (P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
-****)
+\end{verbatim}
+*)
 
 (* Some datatypes at the [Type] level *)