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, 4 deletions

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 1f1ad6ce5..eb7edad11 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -94,12 +94,12 @@ Syntactic Definition ProjS2 := (projS2 ? ?).
 
 Section Extended_booleans.
 
-  (* Syntax sumbool "{_}+{_}". *)
+  (* Syntax sumbool ["{_}+{_}"]. *)
   Inductive sumbool [A,B:Prop] : Set
       := left  : A -> (sumbool A B) 
        | right : B -> (sumbool A B).
 
-  (* Syntax sumor "_+{_}". *)
+  (* Syntax sumor ["_+{_}"]. *)
   Inductive sumor [A:Set;B:Prop] : Set
       := inleft  : A -> (sumor A B) 
        | inright : B -> (sumor A B).
@@ -210,9 +210,9 @@ Proof.
   Intros A B C F AB; Apply F; Elim AB; Auto.
 Qed.
 
-(** is now a theorem
+(*i is now a theorem
 Axiom eq_rec : (A:Set)(a:A)(P:A->Set)(P a)->(b:A) a=b -> (P b).
-**)
+i*)
 
 Hints Resolve left right inleft inright : core v62.