mise a jour

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

3 files changed, 251 insertions, 215 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 3604e5ea6..1dcc8f873 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -3,7 +3,7 @@
 %%For: Gros nain
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 91
+%%BoundingBox: 36 36 577 91
 %%EndComments
 %%BeginProlog
 save
@@ -139,41 +139,41 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 91
+%%PageBoundingBox: 36 36 577 91
 gsave
-35 35 541 56 boxprim clip newpath
+35 35 542 56 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.3994 set_scale
+0.3982 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Univ
 gsave 10 dict begin
-1229 74 27 18 ellipse_path
+1231 101 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1229 75 moveto (Univ) 28 14.00 -0.50 alignedtext
+1231 102 moveto (Univ) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Names
 gsave 10 dict begin
-1322 74 29 18 ellipse_path
+1326 101 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1322 75 moveto (Names) 38 14.00 -0.50 alignedtext
+1326 102 moveto (Names) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Univ -> Names
-newpath 1256 74 moveto
-1264 74 1273 74 1282 74 curveto
+newpath 1258 101 moveto
+1267 101 1277 101 1286 101 curveto
 stroke
-newpath 1282 72 moveto
-1292 74 lineto
-1282 77 lineto
+newpath 1286 99 moveto
+1296 101 lineto
+1286 104 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -282,12 +282,31 @@ end grestore
 end grestore
 
 %	Term -> Univ
-newpath 1166 74 moveto
-1174 74 1183 74 1192 74 curveto
+newpath 1164 81 moveto
+1174 84 1186 88 1197 91 curveto
 stroke
-newpath 1192 72 moveto
-1202 74 lineto
-1192 77 lineto
+newpath 1197 88 moveto
+1206 94 lineto
+1196 93 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Esubst
+gsave 10 dict begin
+1231 47 29 18 ellipse_path
+stroke
+gsave 10 dict begin
+1231 48 moveto (Esubst) 37 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Term -> Esubst
+newpath 1164 67 moveto
+1174 64 1185 61 1196 58 curveto
+stroke
+newpath 1195 56 moveto
+1205 55 lineto
+1196 61 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -359,12 +378,12 @@ gsave 0 setgray stroke grestore fill
 
 %	Cooking -> Reduction
 newpath 300 116 moveto
-336 113 393 108 426 102 curveto
-426 102 444 95 462 87 curveto
+336 114 393 109 426 102 curveto
+437 99 453 94 468 88 curveto
 stroke
-newpath 461 85 moveto
-471 84 lineto
-462 90 lineto
+newpath 464 87 moveto
+474 85 lineto
+466 92 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index 5ee8ccaa0..3507cf4a9 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -3,7 +3,7 @@
 %%For: Gros nain
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 225
+%%BoundingBox: 36 36 576 186
 %%EndComments
 %%BeginProlog
 save
@@ -139,367 +139,365 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 225
+%%PageBoundingBox: 36 36 576 186
 gsave
-35 35 541 190 boxprim clip newpath
+35 35 541 151 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.7050 set_scale
+0.6818 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Pcoq
 gsave 10 dict begin
-643 141 27 18 ellipse_path
+669 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-643 142 moveto (Pcoq) 28 14.00 -0.50 alignedtext
+669 73 moveto (Pcoq) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqast
 gsave 10 dict begin
-736 141 30 18 ellipse_path
+762 72 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-736 142 moveto (Coqast) 38 14.00 -0.50 alignedtext
+762 73 moveto (Coqast) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pcoq -> Coqast
-newpath 670 141 moveto
-678 141 687 141 696 141 curveto
+newpath 696 72 moveto
+704 72 713 72 722 72 curveto
 stroke
-newpath 696 139 moveto
-706 141 lineto
-696 144 lineto
+newpath 722 70 moveto
+732 72 lineto
+722 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Extend
 gsave 10 dict begin
-460 141 30 18 ellipse_path
+486 124 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-460 142 moveto (Extend) 39 14.00 -0.50 alignedtext
+486 125 moveto (Extend) 39 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Ast
 gsave 10 dict begin
-553 141 27 18 ellipse_path
+579 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-553 142 moveto (Ast) 19 14.00 -0.50 alignedtext
+579 73 moveto (Ast) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Extend -> Ast
-newpath 490 141 moveto
-498 141 507 141 516 141 curveto
+newpath 508 112 moveto
+520 105 536 96 550 88 curveto
 stroke
-newpath 516 139 moveto
-526 141 lineto
-516 144 lineto
+newpath 548 86 moveto
+558 84 lineto
+550 91 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Ast -> Pcoq
-newpath 580 141 moveto
-588 141 597 141 606 141 curveto
+newpath 606 72 moveto
+614 72 623 72 632 72 curveto
 stroke
-newpath 606 139 moveto
-616 141 lineto
-606 144 lineto
+newpath 632 70 moveto
+642 72 lineto
+632 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Termast
 gsave 10 dict begin
-354 195 33 18 ellipse_path
+380 18 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-354 196 moveto (Termast) 45 14.00 -0.50 alignedtext
+380 19 moveto (Termast) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Termast -> Ast
-newpath 386 190 moveto
-417 186 463 178 490 171 curveto
-490 171 507 163 523 155 curveto
+newpath 413 22 moveto
+443 25 489 32 516 40 curveto
+526 43 540 50 553 57 curveto
 stroke
-newpath 521 153 moveto
-531 151 lineto
-523 158 lineto
+newpath 551 53 moveto
+559 60 lineto
+549 58 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Search
 gsave 10 dict begin
-30 60 29 18 ellipse_path
+30 46 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-30 61 moveto (Search) 37 14.00 -0.50 alignedtext
+30 47 moveto (Search) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Astterm
 gsave 10 dict begin
-354 33 33 18 ellipse_path
+258 72 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-354 34 moveto (Astterm) 45 14.00 -0.50 alignedtext
+258 73 moveto (Astterm) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Astterm
-newpath 57 53 moveto
-92 45 151 31 186 26 curveto
-217 22 248 25 278 26 curveto
-288 27 301 28 314 29 curveto
-stroke
-newpath 311 26 moveto
-321 30 lineto
-311 31 lineto
+newpath 59 49 moveto
+99 54 171 62 216 67 curveto
+stroke
+newpath 215 64 moveto
+225 68 lineto
+215 69 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pretty
 gsave 10 dict begin
-123 110 27 18 ellipse_path
+136 22 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-123 111 moveto (Pretty) 33 14.00 -0.50 alignedtext
+136 23 moveto (Pretty) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Pretty
-newpath 53 72 moveto
-65 79 80 87 94 94 curveto
+newpath 58 40 moveto
+71 37 87 33 101 30 curveto
 stroke
-newpath 95 92 moveto
-102 99 lineto
-92 96 lineto
+newpath 100 28 moveto
+110 28 lineto
+101 33 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Astterm -> Ast
-newpath 387 35 moveto
-418 38 465 44 490 57 curveto
-509 67 527 95 540 116 curveto
+%	Astterm -> Termast
+newpath 284 61 moveto
+302 53 327 42 346 34 curveto
 stroke
-newpath 542 114 moveto
-544 124 lineto
-537 116 lineto
+newpath 344 32 moveto
+354 30 lineto
+346 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Printer
 gsave 10 dict begin
-232 164 29 18 ellipse_path
+258 18 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-232 165 moveto (Printer) 38 14.00 -0.50 alignedtext
+258 19 moveto (Printer) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pretty -> Printer
-newpath 145 121 moveto
-161 129 183 139 201 149 curveto
+newpath 163 21 moveto
+179 20 200 20 218 19 curveto
 stroke
-newpath 201 146 moveto
-209 153 lineto
-199 151 lineto
+newpath 218 17 moveto
+228 19 lineto
+218 22 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Printer -> Termast
-newpath 259 171 moveto
-275 175 296 180 315 185 curveto
+newpath 288 18 moveto
+303 18 321 18 337 18 curveto
 stroke
-newpath 315 182 moveto
-324 187 lineto
-314 187 lineto
+newpath 337 16 moveto
+347 18 lineto
+337 21 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Esyntax
 gsave 10 dict begin
-354 141 33 18 ellipse_path
+380 180 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-354 142 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+380 181 moveto (Esyntax) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Printer -> Esyntax
-newpath 260 159 moveto
-276 156 296 152 313 149 curveto
-stroke
-newpath 313 147 moveto
-323 147 lineto
-314 151 lineto
+newpath 284 27 moveto
+293 31 301 36 304 42 curveto
+325 76 321 121 340 156 curveto
+342 160 345 163 350 165 curveto
+stroke
+newpath 348 161 moveto
+356 168 lineto
+346 166 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Esyntax -> Extend
-newpath 387 141 moveto
-398 141 410 141 421 141 curveto
+newpath 404 167 moveto
+419 159 439 149 455 140 curveto
 stroke
-newpath 420 139 moveto
-430 141 lineto
-420 144 lineto
+newpath 453 138 moveto
+463 136 lineto
+455 143 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_zsyntax
 gsave 10 dict begin
-232 110 40 18 ellipse_path
+136 136 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-232 111 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
+136 137 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_zsyntax -> Astterm
-newpath 259 97 moveto
-266 93 273 89 278 86 curveto
-291 77 302 65 314 57 curveto
-317 55 319 54 322 52 curveto
-stroke
-newpath 321 49 moveto
-331 46 lineto
-324 54 lineto
+newpath 162 122 moveto
+180 112 206 99 226 88 curveto
+stroke
+newpath 224 86 moveto
+234 84 lineto
+226 91 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_zsyntax -> Esyntax
-newpath 267 119 moveto
-282 123 300 127 315 131 curveto
+newpath 170 146 moveto
+185 150 201 154 212 156 curveto
+247 163 302 170 340 175 curveto
 stroke
-newpath 315 128 moveto
-324 133 lineto
-314 133 lineto
+newpath 338 172 moveto
+348 176 lineto
+338 177 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_rsyntax
 gsave 10 dict begin
-232 56 39 18 ellipse_path
+136 200 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-232 57 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
+136 201 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_rsyntax -> Astterm
-newpath 269 49 moveto
-283 47 299 43 313 41 curveto
-stroke
-newpath 313 39 moveto
-323 39 lineto
-314 43 lineto
+newpath 157 185 moveto
+164 179 172 172 176 166 curveto
+192 144 195 115 212 96 curveto
+212 96 218 93 225 89 curveto
+stroke
+newpath 224 87 moveto
+234 85 lineto
+226 91 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_rsyntax -> Esyntax
-newpath 260 69 moveto
-267 72 274 76 278 80 curveto
-292 90 301 106 314 117 curveto
-317 119 319 120 322 122 curveto
-stroke
-newpath 324 120 moveto
-331 128 lineto
-321 125 lineto
+newpath 175 197 moveto
+220 193 292 187 338 184 curveto
+stroke
+newpath 337 182 moveto
+347 183 lineto
+337 187 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax
 gsave 10 dict begin
-232 218 45 18 ellipse_path
+258 126 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-232 219 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
+258 127 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_natsyntax -> Termast
-newpath 273 210 moveto
-286 208 301 205 314 203 curveto
-stroke
-newpath 313 201 moveto
-323 201 lineto
-314 206 lineto
+newpath 288 113 moveto
+295 109 300 106 304 102 curveto
+321 85 325 59 340 42 curveto
+343 39 345 37 348 36 curveto
+stroke
+newpath 347 34 moveto
+357 31 lineto
+349 38 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax -> Esyntax
-newpath 261 204 moveto
-267 200 274 197 278 194 curveto
-291 185 302 173 314 165 curveto
-314 165 318 163 323 159 curveto
-stroke
-newpath 322 157 moveto
-332 154 lineto
-324 161 lineto
+newpath 288 139 moveto
+306 147 328 157 346 165 curveto
+stroke
+newpath 346 162 moveto
+355 168 lineto
+345 167 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Stdlib
+%	Coqlib
 gsave 10 dict begin
-354 249 27 18 ellipse_path
+380 126 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-354 250 moveto (Stdlib) 33 14.00 -0.50 alignedtext
+380 127 moveto (Coqlib) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	G_natsyntax -> Stdlib
-newpath 271 228 moveto
-287 232 305 236 320 240 curveto
+%	G_natsyntax -> Coqlib
+newpath 304 126 moveto
+316 126 329 126 340 126 curveto
 stroke
-newpath 320 237 moveto
-329 243 lineto
-319 242 lineto
+newpath 340 124 moveto
+350 126 lineto
+340 129 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Egrammar
 gsave 10 dict begin
-354 87 40 18 ellipse_path
+380 72 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-354 88 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+380 73 moveto (Egrammar) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Egrammar -> Extend
-newpath 381 101 moveto
-395 109 413 118 429 125 curveto
+newpath 407 85 moveto
+421 93 439 101 454 108 curveto
 stroke
-newpath 429 122 moveto
-437 129 lineto
-427 127 lineto
+newpath 454 105 moveto
+462 112 lineto
+452 110 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Lexer
 gsave 10 dict begin
-460 87 27 18 ellipse_path
+486 70 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-460 88 moveto (Lexer) 32 14.00 -0.50 alignedtext
+486 71 moveto (Lexer) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Egrammar -> Lexer
-newpath 394 87 moveto
-404 87 414 87 423 87 curveto
+newpath 420 71 moveto
+430 71 440 71 449 71 curveto
 stroke
-newpath 423 85 moveto
-433 87 lineto
-423 90 lineto
+newpath 449 69 moveto
+459 71 lineto
+449 74 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index e18d3dd57..c54821490 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -3,7 +3,7 @@
 %%For: Gros nain
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 238
+%%BoundingBox: 36 36 576 216
 %%EndComments
 %%BeginProlog
 save
@@ -139,12 +139,12 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 238
+%%PageBoundingBox: 36 36 576 216
 gsave
-35 35 541 203 boxprim clip newpath
+35 35 541 181 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.7219 set_scale
+0.6444 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
@@ -196,6 +196,34 @@ newpath 541 244 moveto
 closepath
 gsave 0 setgray stroke grestore fill
 
+%	Tacred
+gsave 10 dict begin
+712 72 29 18 ellipse_path
+stroke
+gsave 10 dict begin
+712 73 moveto (Tacred) 38 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Cbv
+gsave 10 dict begin
+811 72 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+811 73 moveto (Cbv) 23 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Tacred -> Cbv
+newpath 742 72 moveto
+752 72 764 72 774 72 curveto
+stroke
+newpath 774 70 moveto
+784 72 lineto
+774 75 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
 %	Syntax_def
 gsave 10 dict begin
 588 207 42 18 ellipse_path
@@ -245,18 +273,28 @@ end grestore
 %	Recordops -> Classops
 newpath 485 112 moveto
 491 108 496 105 500 102 curveto
-514 92 523 77 536 69 curveto
-540 66 546 64 551 61 curveto
+514 93 523 78 536 69 curveto
+541 66 548 63 555 60 curveto
+stroke
+newpath 551 59 moveto
+561 57 lineto
+553 64 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Classops -> Tacred
+newpath 620 52 moveto
+637 55 657 60 675 64 curveto
 stroke
-newpath 550 59 moveto
-560 56 lineto
-552 63 lineto
+newpath 675 61 moveto
+684 66 lineto
+674 66 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Classops -> Rawterm
-newpath 614 57 moveto
-627 63 640 69 640 69 curveto
+newpath 616 56 moveto
+625 60 635 64 640 69 curveto
 656 83 678 109 694 129 curveto
 stroke
 newpath 695 126 moveto
@@ -267,39 +305,20 @@ gsave 0 setgray stroke grestore fill
 
 %	Retyping
 gsave 10 dict begin
-712 72 36 18 ellipse_path
+712 18 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-712 73 moveto (Retyping) 51 14.00 -0.50 alignedtext
+712 19 moveto (Retyping) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Classops -> Retyping
-newpath 620 52 moveto
-635 55 653 59 669 63 curveto
-stroke
-newpath 670 61 moveto
-679 65 lineto
-669 65 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Tacred
-gsave 10 dict begin
-712 18 29 18 ellipse_path
-stroke
-gsave 10 dict begin
-712 19 moveto (Tacred) 38 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Classops -> Tacred
 newpath 620 38 moveto
-637 35 657 30 675 26 curveto
+635 35 653 31 669 27 curveto
 stroke
-newpath 674 24 moveto
-684 24 lineto
-675 29 lineto
+newpath 669 25 moveto
+679 25 lineto
+670 29 lineto
 closepath
 gsave 0 setgray stroke grestore fill