MAJ V7.2

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

1 files changed, 221 insertions, 158 deletions

diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index 9a6de4273..b3ca2ae16 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (clrenard) Clement Renard
+%%For: (herbelin) Hugo Herbelin
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 232
+%%BoundingBox: 36 36 576 330
 %%EndComments
 %%BeginProlog
 save
@@ -150,379 +150,442 @@ def
 %%EndResource
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 232
+%%PageBoundingBox: 36 36 576 330
 %%PageOrientation: Portrait
 gsave
-35 35 541 197 boxprim clip newpath
+35 35 541 295 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.7584 set_scale
+0.7479 set_scale
 0 0 translate 0 rotate
-[ /CropBox [36 36 576 232] /PAGES pdfmark
+[ /CropBox [36 36 576 330] /PAGES pdfmark
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Pcoq
 gsave 10 dict begin
-581 103 27 18 ellipse_path
+591 251 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-581 104 moveto (Pcoq) 28 14.00 -0.50 alignedtext
+591 252 moveto (Pcoq) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqast
 gsave 10 dict begin
-674 103 30 18 ellipse_path
+684 251 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-674 104 moveto (Coqast) 38 14.00 -0.50 alignedtext
+684 252 moveto (Coqast) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pcoq -> Coqast
-newpath 608 103 moveto
-616 103 625 103 634 103 curveto
+newpath 618 251 moveto
+626 251 635 251 644 251 curveto
 stroke
-newpath 634 101 moveto
-644 103 lineto
-634 106 lineto
+newpath 644 249 moveto
+654 251 lineto
+644 254 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Extend
 gsave 10 dict begin
-398 52 30 18 ellipse_path
+405 224 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-398 53 moveto (Extend) 39 14.00 -0.50 alignedtext
+405 225 moveto (Extend) 39 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Ast
 gsave 10 dict begin
-491 103 27 18 ellipse_path
+501 251 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-491 104 moveto (Ast) 19 14.00 -0.50 alignedtext
+501 252 moveto (Ast) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Extend -> Ast
-newpath 421 64 moveto
-433 71 448 79 462 86 curveto
+newpath 432 232 moveto
+443 235 455 238 467 241 curveto
 stroke
-newpath 463 84 moveto
-470 91 lineto
-460 88 lineto
+newpath 467 238 moveto
+476 244 lineto
+466 243 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Ast -> Pcoq
-newpath 518 103 moveto
-526 103 535 103 544 103 curveto
+newpath 528 251 moveto
+536 251 545 251 554 251 curveto
 stroke
-newpath 544 101 moveto
-554 103 lineto
-544 106 lineto
+newpath 554 249 moveto
+564 251 lineto
+554 254 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Termast
 gsave 10 dict begin
-292 156 33 18 ellipse_path
+405 278 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-292 157 moveto (Termast) 45 14.00 -0.50 alignedtext
+405 279 moveto (Termast) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Termast -> Ast
-newpath 325 152 moveto
-355 149 401 143 428 136 curveto
-438 133 451 127 462 120 curveto
+newpath 435 270 moveto
+445 267 456 264 467 261 curveto
 stroke
-newpath 461 118 moveto
-471 115 lineto
-463 122 lineto
+newpath 466 259 moveto
+476 258 lineto
+467 264 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Search
 gsave 10 dict begin
-48 198 29 18 ellipse_path
+39 305 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-48 199 moveto (Search) 37 14.00 -0.50 alignedtext
+39 306 moveto (Search) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Astterm
 gsave 10 dict begin
-170 94 33 18 ellipse_path
+296 170 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-170 95 moveto (Astterm) 45 14.00 -0.50 alignedtext
+296 171 moveto (Astterm) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Astterm
-newpath 71 186 moveto
-78 183 84 178 88 174 curveto
-104 157 109 133 124 118 curveto
-127 115 132 112 137 109 curveto
-stroke
-newpath 134 108 moveto
-144 106 lineto
-136 112 lineto
+newpath 61 293 moveto
+65 289 69 285 70 281 curveto
+90 199 63 103 106 32 curveto
+126 0 190 10 220 32 curveto
+252 57 237 111 256 146 curveto
+258 149 260 151 263 153 curveto
+stroke
+newpath 264 151 moveto
+272 157 lineto
+262 155 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqlib
 gsave 10 dict begin
-292 229 29 18 ellipse_path
+296 374 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-292 230 moveto (Coqlib) 38 14.00 -0.50 alignedtext
+296 375 moveto (Coqlib) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Coqlib
-newpath 70 210 moveto
-87 218 109 229 124 232 curveto
-159 239 217 235 255 233 curveto
+newpath 53 321 moveto
+67 336 88 357 106 362 curveto
+146 372 215 375 257 374 curveto
 stroke
-newpath 253 231 moveto
-263 232 lineto
-253 236 lineto
+newpath 256 372 moveto
+266 374 lineto
+256 377 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Printer
 gsave 10 dict begin
-170 148 29 18 ellipse_path
+163 278 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-170 149 moveto (Printer) 38 14.00 -0.50 alignedtext
+163 279 moveto (Printer) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Printer
-newpath 73 188 moveto
-91 180 116 170 137 162 curveto
+newpath 67 299 moveto
+84 296 107 291 126 286 curveto
 stroke
-newpath 135 160 moveto
-145 158 lineto
-137 165 lineto
+newpath 125 284 moveto
+135 284 lineto
+126 289 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Astterm -> Termast
-newpath 194 106 moveto
-213 116 239 129 260 139 curveto
-stroke
-newpath 260 136 moveto
-268 143 lineto
-258 141 lineto
+newpath 321 182 moveto
+327 186 333 190 336 194 curveto
+352 211 358 235 372 254 curveto
+374 256 376 258 378 260 curveto
+stroke
+newpath 377 256 moveto
+384 264 lineto
+374 261 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Printer -> Termast
-newpath 200 150 moveto
-215 151 233 152 249 153 curveto
+newpath 193 278 moveto
+235 278 314 278 362 278 curveto
 stroke
-newpath 249 151 moveto
-259 154 lineto
-249 155 lineto
+newpath 362 276 moveto
+372 278 lineto
+362 281 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Esyntax
 gsave 10 dict begin
-292 48 33 18 ellipse_path
+296 224 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-292 49 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+296 225 moveto (Esyntax) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Printer -> Esyntax
-newpath 194 137 moveto
-203 133 211 128 216 124 curveto
-232 109 238 86 252 72 curveto
-254 70 256 68 259 66 curveto
-stroke
-newpath 258 64 moveto
-268 61 lineto
-260 68 lineto
+newpath 188 268 moveto
+208 259 237 247 260 238 curveto
+stroke
+newpath 259 236 moveto
+269 235 lineto
+260 241 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Esyntax -> Extend
-newpath 325 49 moveto
-336 49 348 50 359 50 curveto
+newpath 329 224 moveto
+340 224 353 224 365 224 curveto
 stroke
-newpath 358 47 moveto
-368 51 lineto
-358 52 lineto
+newpath 365 222 moveto
+375 224 lineto
+365 227 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Prettyp
 gsave 10 dict begin
-48 144 30 18 ellipse_path
+39 251 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-48 145 moveto (Prettyp) 40 14.00 -0.50 alignedtext
+39 252 moveto (Prettyp) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Prettyp -> Printer
-newpath 78 145 moveto
-94 146 114 146 131 147 curveto
+newpath 68 257 moveto
+85 260 107 265 126 270 curveto
 stroke
-newpath 130 145 moveto
-140 147 lineto
-130 150 lineto
+newpath 126 267 moveto
+135 272 lineto
+125 272 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_zsyntax
 gsave 10 dict begin
-48 86 40 18 ellipse_path
+163 224 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-48 87 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
+163 225 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_zsyntax -> Astterm
-newpath 88 89 moveto
-101 90 115 91 128 91 curveto
+newpath 193 212 moveto
+213 204 240 193 261 184 curveto
 stroke
-newpath 127 88 moveto
-137 92 lineto
-127 93 lineto
+newpath 259 182 moveto
+269 181 lineto
+261 187 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_zsyntax -> Esyntax
-newpath 80 75 moveto
-95 71 112 66 124 64 curveto
-159 58 214 54 251 51 curveto
+newpath 203 224 moveto
+219 224 237 224 254 224 curveto
+stroke
+newpath 253 222 moveto
+263 224 lineto
+253 227 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	G_string_syntax
+gsave 10 dict begin
+163 170 56 18 ellipse_path
+stroke
+gsave 10 dict begin
+163 171 moveto (G_string_syntax) 92 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	G_string_syntax -> Astterm
+newpath 220 170 moveto
+232 170 243 170 254 170 curveto
+stroke
+newpath 253 168 moveto
+263 170 lineto
+253 173 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	G_string_syntax -> Esyntax
+newpath 198 184 moveto
+217 192 242 202 261 210 curveto
 stroke
-newpath 249 49 moveto
-259 50 lineto
-249 54 lineto
+newpath 261 207 moveto
+269 213 lineto
+259 212 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_rsyntax
 gsave 10 dict begin
-48 25 39 18 ellipse_path
+163 116 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-48 26 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
+163 117 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_rsyntax -> Astterm
-newpath 73 39 moveto
-92 50 119 65 139 77 curveto
+newpath 193 128 moveto
+213 136 240 147 261 156 curveto
 stroke
-newpath 139 74 moveto
-147 81 lineto
-137 79 lineto
+newpath 261 153 moveto
+269 159 lineto
+259 158 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_rsyntax -> Esyntax
-newpath 88 26 moveto
-126 26 182 28 216 31 curveto
-226 32 242 35 255 38 curveto
-stroke
-newpath 253 35 moveto
-262 40 lineto
-252 40 lineto
+newpath 192 128 moveto
+206 134 220 140 220 140 curveto
+238 155 241 182 256 200 curveto
+258 202 260 204 263 206 curveto
+stroke
+newpath 264 204 moveto
+272 211 lineto
+262 208 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax
 gsave 10 dict begin
-170 202 45 18 ellipse_path
+163 332 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-170 203 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
+163 333 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_natsyntax -> Termast
-newpath 203 190 moveto
-219 184 239 176 256 169 curveto
+newpath 203 323 moveto
+248 313 320 297 365 287 curveto
 stroke
-newpath 255 167 moveto
-265 166 lineto
-256 172 lineto
+newpath 364 285 moveto
+374 285 lineto
+365 290 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax -> Coqlib
-newpath 210 211 moveto
-225 214 241 218 255 221 curveto
+newpath 199 343 moveto
+218 349 242 357 261 363 curveto
 stroke
-newpath 255 218 moveto
-264 223 lineto
-254 223 lineto
+newpath 261 360 moveto
+270 366 lineto
+260 365 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax -> Esyntax
-newpath 201 189 moveto
-207 186 213 183 216 178 curveto
-236 146 234 104 252 72 curveto
-252 72 256 70 261 66 curveto
-stroke
-newpath 260 64 moveto
-270 61 lineto
-262 68 lineto
+newpath 197 320 moveto
+206 316 214 312 220 308 curveto
+238 294 261 267 277 248 curveto
+stroke
+newpath 275 247 moveto
+283 241 lineto
+278 250 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	G_ascii_syntax
+gsave 10 dict begin
+163 62 53 18 ellipse_path
+stroke
+gsave 10 dict begin
+163 63 moveto (G_ascii_syntax) 86 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	G_ascii_syntax -> Astterm
+newpath 201 75 moveto
+209 78 216 82 220 86 curveto
+238 101 241 128 256 146 curveto
+258 148 260 150 263 152 curveto
+stroke
+newpath 264 150 moveto
+272 157 lineto
+262 154 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	G_ascii_syntax -> Esyntax
+newpath 203 74 moveto
+210 77 216 80 220 86 curveto
+243 119 237 165 256 200 curveto
+258 203 260 205 263 207 curveto
+stroke
+newpath 264 205 moveto
+272 211 lineto
+262 209 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Egrammar
 gsave 10 dict begin
-292 102 40 18 ellipse_path
+296 116 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-292 103 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+296 117 moveto (Egrammar) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Egrammar -> Extend
-newpath 320 89 moveto
-334 82 351 74 366 67 curveto
+newpath 320 131 moveto
+329 136 336 140 336 140 curveto
+351 155 372 181 388 201 curveto
 stroke
-newpath 364 65 moveto
-374 63 lineto
-366 70 lineto
+newpath 389 198 moveto
+393 208 lineto
+385 201 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Lexer
 gsave 10 dict begin
-398 106 27 18 ellipse_path
+405 116 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-398 107 moveto (Lexer) 32 14.00 -0.50 alignedtext
+405 117 moveto (Lexer) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Egrammar -> Lexer
-newpath 332 104 moveto
-342 104 352 105 361 105 curveto
+newpath 336 116 moveto
+347 116 358 116 368 116 curveto
 stroke
-newpath 361 103 moveto
-371 105 lineto
-361 108 lineto
+newpath 368 114 moveto
+378 116 lineto
+368 119 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage