traducteur: affiche les commentaires a l'interieur des commandes

extraction: pb avec les variables de section definies


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

3 files changed, 3 insertions, 3 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 03b7c06f0..65d0722c3 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -80,8 +80,8 @@ Notation Snd := (snd ? ?).
 
 Hints Resolve pair inl inr : core v62.
 
-(** Parsing only of things in [Datatypes.v] *)
 V7only[
+(** Parsing only of things in [Datatypes.v] *)
 Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot).
 Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot).
 Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot).
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 21dd4ccec..e48b15062 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -40,9 +40,9 @@ Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q)
   V8only "'EXT2' x : t | p & q" (at level 200, x at level 80).
 ].
 
-(** Parsing only of things in [Logic_type.v] *)
 
 V7only[
+(** Parsing only of things in [Logic_type.v] *)
 Notation "< A > x == y"  := (eq A x y)
    (A annot, at level 1, x at level 0, only parsing).
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index e5b516090..41f26ffda 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -205,8 +205,8 @@ Syntax constr
   | O [ O ]      -> ["(0)"].
 ].
 
-(* For parsing/printing based on scopes *)
 V7only [
+(* For parsing/printing based on scopes *)
 Module nat_scope.
 Infix 4 "+" plus : nat_scope.
 Infix 3 "*" mult : nat_scope.