diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-22 18:09:11 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-22 18:09:11 +0000 |
| commit | 66ee7ba58080fa8fcfdb4bb76b89cc0b70a8a4ac (patch) | |
| tree | e97e3bd30fa49fc5da4dfe207ff73e841ee083b1 /theories/Init/Peano.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/Peano.v')
| -rwxr-xr-x | theories/Init/Peano.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |