MAJ V7.2

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

7 files changed, 386 insertions, 321 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 6b7d42d89..e707a62c8 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.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 577 73
+%%BoundingBox: 36 36 576 70
 %%EndComments
 %%BeginProlog
 save
@@ -150,43 +150,43 @@ def
 %%EndResource
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 73
+%%PageBoundingBox: 36 36 576 70
 %%PageOrientation: Portrait
 gsave
-35 35 542 38 boxprim clip newpath
+35 35 541 35 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.3953 set_scale
+0.3614 set_scale
 0 0 translate 0 rotate
-[ /CropBox [36 36 577 73] /PAGES pdfmark
+[ /CropBox [36 36 576 70] /PAGES pdfmark
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Univ
 gsave 10 dict begin
-1233 74 27 18 ellipse_path
+1361 74 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1233 75 moveto (Univ) 28 14.00 -0.50 alignedtext
+1361 75 moveto (Univ) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Names
 gsave 10 dict begin
-1328 74 29 18 ellipse_path
+1456 74 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1328 75 moveto (Names) 38 14.00 -0.50 alignedtext
+1456 75 moveto (Names) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Univ -> Names
-newpath 1260 74 moveto
-1269 74 1279 74 1288 74 curveto
+newpath 1388 74 moveto
+1397 74 1407 74 1416 74 curveto
 stroke
-newpath 1288 72 moveto
-1298 74 lineto
-1288 77 lineto
+newpath 1416 72 moveto
+1426 74 lineto
+1416 77 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -256,18 +256,18 @@ newpath 574 36 moveto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Closure
+%	Conv_oracle
 gsave 10 dict begin
-726 47 32 18 ellipse_path
+740 47 46 18 ellipse_path
 stroke
 gsave 10 dict begin
-726 48 moveto (Closure) 43 14.00 -0.50 alignedtext
+740 48 moveto (Conv_oracle) 71 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Reduction -> Closure
+%	Reduction -> Conv_oracle
 newpath 658 47 moveto
-667 47 676 47 684 47 curveto
+667 47 675 47 684 47 curveto
 stroke
 newpath 684 45 moveto
 694 47 lineto
@@ -277,58 +277,58 @@ gsave 0 setgray stroke grestore fill
 
 %	Term
 gsave 10 dict begin
-1141 47 27 18 ellipse_path
+1269 47 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1141 48 moveto (Term) 30 14.00 -0.50 alignedtext
+1269 48 moveto (Term) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Univ
-newpath 1166 54 moveto
-1176 57 1188 61 1199 64 curveto
+newpath 1294 54 moveto
+1304 57 1316 61 1327 64 curveto
 stroke
-newpath 1199 61 moveto
-1208 67 lineto
-1198 66 lineto
+newpath 1327 61 moveto
+1336 67 lineto
+1326 66 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Esubst
 gsave 10 dict begin
-1233 20 29 18 ellipse_path
+1361 20 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1233 21 moveto (Esubst) 37 14.00 -0.50 alignedtext
+1361 21 moveto (Esubst) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Esubst
-newpath 1166 40 moveto
-1176 37 1187 34 1198 31 curveto
+newpath 1294 40 moveto
+1304 37 1315 34 1326 31 curveto
 stroke
-newpath 1197 29 moveto
-1207 28 lineto
-1198 34 lineto
+newpath 1325 29 moveto
+1335 28 lineto
+1326 34 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sign
 gsave 10 dict begin
-1051 47 27 18 ellipse_path
+1179 47 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1051 48 moveto (Sign) 25 14.00 -0.50 alignedtext
+1179 48 moveto (Sign) 25 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sign -> Term
-newpath 1078 47 moveto
-1086 47 1095 47 1104 47 curveto
+newpath 1206 47 moveto
+1214 47 1223 47 1232 47 curveto
 stroke
-newpath 1104 45 moveto
-1114 47 lineto
-1104 50 lineto
+newpath 1232 45 moveto
+1242 47 lineto
+1232 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -399,51 +399,70 @@ newpath 229 18 moveto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Environ
+%	Closure
 gsave 10 dict begin
-827 47 33 18 ellipse_path
+854 47 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-827 48 moveto (Environ) 45 14.00 -0.50 alignedtext
+854 48 moveto (Closure) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Closure -> Environ
-newpath 758 47 moveto
-766 47 775 47 784 47 curveto
+%	Conv_oracle -> Closure
+newpath 786 47 moveto
+795 47 804 47 812 47 curveto
 stroke
-newpath 784 45 moveto
-794 47 lineto
-784 50 lineto
+newpath 812 45 moveto
+822 47 lineto
+812 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
+%	Environ
+gsave 10 dict begin
+955 47 33 18 ellipse_path
+stroke
+gsave 10 dict begin
+955 48 moveto (Environ) 45 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
 %	Declarations
 gsave 10 dict begin
-942 47 45 18 ellipse_path
+1070 47 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-942 48 moveto (Declarations) 70 14.00 -0.50 alignedtext
+1070 48 moveto (Declarations) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Declarations
-newpath 860 47 moveto
-868 47 877 47 886 47 curveto
+newpath 988 47 moveto
+996 47 1005 47 1014 47 curveto
 stroke
-newpath 886 45 moveto
-896 47 lineto
-886 50 lineto
+newpath 1014 45 moveto
+1024 47 lineto
+1014 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declarations -> Sign
-newpath 988 47 moveto
-997 47 1006 47 1014 47 curveto
+newpath 1116 47 moveto
+1125 47 1134 47 1142 47 curveto
 stroke
-newpath 1014 45 moveto
-1024 47 lineto
-1014 50 lineto
+newpath 1142 45 moveto
+1152 47 lineto
+1142 50 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Closure -> Environ
+newpath 886 47 moveto
+894 47 903 47 912 47 curveto
+stroke
+newpath 912 45 moveto
+922 47 lineto
+912 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index f79236717..4f9297273 100644
--- a/doc/library.dep.ps
+++ b/doc/library.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 543 235
+%%BoundingBox: 36 36 543 181
 %%EndComments
 %%BeginProlog
 save
@@ -150,14 +150,14 @@ def
 %%EndResource
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 543 235
+%%PageBoundingBox: 36 36 543 181
 %%PageOrientation: Portrait
 gsave
-35 35 508 200 boxprim clip newpath
+35 35 508 146 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
 0 0 translate 0 rotate
-[ /CropBox [36 36 543 235] /PAGES pdfmark
+[ /CropBox [36 36 543 181] /PAGES pdfmark
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
@@ -191,144 +191,127 @@ gsave 0 setgray stroke grestore fill
 
 %	Global
 gsave 10 dict begin
-246 126 29 18 ellipse_path
+246 99 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-246 127 moveto (Global) 38 14.00 -0.50 alignedtext
+246 100 moveto (Global) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Library -> Global
-newpath 175 126 moveto
-185 126 196 126 206 126 curveto
+newpath 172 118 moveto
+184 115 197 112 210 108 curveto
 stroke
-newpath 206 124 moveto
-216 126 lineto
-206 129 lineto
+newpath 209 106 moveto
+219 106 lineto
+210 111 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Lib
 gsave 10 dict begin
-246 72 27 18 ellipse_path
+246 45 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-246 73 moveto (Lib) 19 14.00 -0.50 alignedtext
+246 46 moveto (Lib) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Library -> Lib
-newpath 167 114 moveto
-181 106 201 96 217 87 curveto
+newpath 165 112 moveto
+171 109 176 105 180 102 curveto
+193 91 204 79 216 69 curveto
+218 67 220 65 223 63 curveto
 stroke
-newpath 215 85 moveto
-225 83 lineto
-217 90 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Opaque
-gsave 10 dict begin
-144 180 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-144 181 moveto (Opaque) 43 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Opaque -> Global
-newpath 167 168 moveto
-181 160 200 151 216 142 curveto
-stroke
-newpath 214 140 moveto
-224 138 lineto
-216 145 lineto
+newpath 219 62 moveto
+229 59 lineto
+222 67 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Nametab
 gsave 10 dict begin
-349 126 35 18 ellipse_path
+349 99 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-349 127 moveto (Nametab) 50 14.00 -0.50 alignedtext
+349 100 moveto (Nametab) 50 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Global -> Nametab
-newpath 276 126 moveto
-285 126 294 126 303 126 curveto
-stroke
-newpath 303 124 moveto
-313 126 lineto
-303 129 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
 %	Nameops
 gsave 10 dict begin
-460 153 36 18 ellipse_path
+460 126 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-460 154 moveto (Nameops) 52 14.00 -0.50 alignedtext
+460 127 moveto (Nameops) 52 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Nametab -> Nameops
-newpath 381 134 moveto
-392 137 405 140 417 143 curveto
+newpath 381 107 moveto
+392 110 405 113 417 116 curveto
 stroke
-newpath 418 141 moveto
-427 145 lineto
-417 145 lineto
+newpath 418 114 moveto
+427 118 lineto
+417 118 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Summary
 gsave 10 dict begin
-460 99 37 18 ellipse_path
+460 72 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-460 100 moveto (Summary) 54 14.00 -0.50 alignedtext
+460 73 moveto (Summary) 54 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Nametab -> Summary
-newpath 381 118 moveto
-392 116 405 112 417 109 curveto
+newpath 381 91 moveto
+392 89 405 85 417 82 curveto
+stroke
+newpath 416 80 moveto
+426 80 lineto
+417 85 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Global -> Nametab
+newpath 276 99 moveto
+285 99 294 99 303 99 curveto
 stroke
-newpath 416 107 moveto
-426 107 lineto
-417 112 lineto
+newpath 303 97 moveto
+313 99 lineto
+303 102 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Lib -> Nametab
-newpath 267 83 moveto
-281 91 300 100 316 109 curveto
+newpath 267 56 moveto
+281 64 300 73 316 82 curveto
 stroke
-newpath 316 106 moveto
-324 113 lineto
-314 111 lineto
+newpath 316 79 moveto
+324 86 lineto
+314 84 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Libobject
 gsave 10 dict begin
-349 72 37 18 ellipse_path
+349 45 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-349 73 moveto (Libobject) 53 14.00 -0.50 alignedtext
+349 46 moveto (Libobject) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Lib -> Libobject
-newpath 273 72 moveto
-282 72 292 72 302 72 curveto
+newpath 273 45 moveto
+282 45 292 45 302 45 curveto
 stroke
-newpath 302 70 moveto
-312 72 lineto
-302 75 lineto
+newpath 302 43 moveto
+312 45 lineto
+302 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -342,22 +325,22 @@ end grestore
 end grestore
 
 %	Impargs -> Global
-newpath 168 85 moveto
-182 93 200 102 215 110 curveto
+newpath 174 80 moveto
+185 83 198 86 210 89 curveto
 stroke
-newpath 215 107 moveto
-223 114 lineto
-213 112 lineto
+newpath 210 86 moveto
+219 92 lineto
+209 91 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Impargs -> Lib
-newpath 177 72 moveto
-188 72 199 72 209 72 curveto
+newpath 174 64 moveto
+186 61 199 57 212 54 curveto
 stroke
-newpath 209 70 moveto
-219 72 lineto
-209 75 lineto
+newpath 211 52 moveto
+221 52 lineto
+212 57 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -372,23 +355,23 @@ end grestore
 
 %	Goptions -> Global
 newpath 166 32 moveto
-172 35 176 38 180 42 curveto
-196 60 202 84 216 102 curveto
-217 103 218 104 219 105 curveto
+171 36 176 39 180 42 curveto
+193 53 204 65 216 75 curveto
+218 77 220 78 223 80 curveto
 stroke
-newpath 221 104 moveto
-227 112 lineto
-218 107 lineto
+newpath 223 76 moveto
+228 85 lineto
+219 80 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Goptions -> Lib
-newpath 169 31 moveto
-183 39 201 48 217 57 curveto
+newpath 176 26 moveto
+188 29 200 32 212 35 curveto
 stroke
-newpath 217 54 moveto
-225 61 lineto
-215 59 lineto
+newpath 212 32 moveto
+221 38 lineto
+211 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
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
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index 9246e91a5..8af063428 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -1,6 +1,6 @@
 %!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 577 203
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index 29c50d955..68b602755 100644
--- a/doc/proofs.dep.ps
+++ b/doc/proofs.dep.ps
@@ -1,6 +1,6 @@
 %!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 577 136
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index 0ec3a8272..a628a56d9 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,6 +1,6 @@
 %!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 577 125
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index 44a92446d..d05a3aba8 100644
--- a/doc/toplevel.dep.ps
+++ b/doc/toplevel.dep.ps
@@ -1,6 +1,6 @@
 %!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 256