From 66ee7ba58080fa8fcfdb4bb76b89cc0b70a8a4ac Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 22 Sep 2003 18:09:11 +0000
Subject: 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
---
 theories/Init/Datatypes.v        | 2 +-
 theories/Init/Logic_TypeSyntax.v | 2 +-
 theories/Init/Peano.v            | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories')

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 03b7c06f08..65d0722c3c 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 21dd4ccec6..e48b150622 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 e5b516090b..41f26ffda9 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.
-- 
cgit v1.2.3