diff options
| author | barras | 2003-09-22 18:09:11 +0000 |
|---|---|---|
| committer | barras | 2003-09-22 18:09:11 +0000 |
| commit | 66ee7ba58080fa8fcfdb4bb76b89cc0b70a8a4ac (patch) | |
| tree | e97e3bd30fa49fc5da4dfe207ff73e841ee083b1 /theories/Init/Datatypes.v | |
| parent | fe027346f901f26d79ce243a06c08a8c9f661e81 (diff) | |
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
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rwxr-xr-x | theories/Init/Datatypes.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |