Minor correction for Ocamlweb + doc update

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

7 files changed, 1001 insertions, 907 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 8a9253ae9..7b6640611 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jc) Jean-Christophe,,,,
+%%For: (jacek) Jacek Chrzaszcz
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 94
+%%BoundingBox: 36 36 577 70
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(() show i str cvs show (,) show j str cvs show ()) show
+			(\() show i str cvs show (,) show j str cvs show (\)) show
 		grestore
 	} if
 } bind def
@@ -139,385 +139,298 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 94
+%%PageBoundingBox: 36 36 577 70
 gsave
-35 35 542 59 boxprim clip newpath
+35 35 542 35 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.4000 set_scale
+0.3745 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
-1221 72 27 18 ellipse_path
+1319 45 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1221 73 moveto (Univ) 28 14.00 -0.50 alignedtext
+1319 46 moveto (Univ) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Names
 gsave 10 dict begin
-1320 45 29 18 ellipse_path
+1412 45 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1320 46 moveto (Names) 38 14.00 -0.50 alignedtext
+1412 46 moveto (Names) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Univ -> Names
-newpath 1246 65 moveto
-1258 62 1271 58 1284 55 curveto
+newpath 1346 45 moveto
+1354 45 1363 45 1372 45 curveto
 stroke
-newpath 1283 53 moveto
-1293 52 lineto
-1284 58 lineto
+newpath 1372 43 moveto
+1382 45 lineto
+1372 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Typeops
 gsave 10 dict begin
-265 70 34 18 ellipse_path
+265 45 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-265 71 moveto (Typeops) 48 14.00 -0.50 alignedtext
+265 46 moveto (Typeops) 48 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Reduction
+%	Inductive
 gsave 10 dict begin
-375 97 39 18 ellipse_path
+381 72 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-375 98 moveto (Reduction) 57 14.00 -0.50 alignedtext
+381 73 moveto (Inductive) 52 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Typeops -> Reduction
-newpath 296 78 moveto
-307 80 319 83 330 86 curveto
+%	Typeops -> Inductive
+newpath 297 52 moveto
+310 55 325 58 339 62 curveto
 stroke
-newpath 331 84 moveto
-340 89 lineto
-330 89 lineto
+newpath 339 59 moveto
+348 64 lineto
+338 64 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Type_errors
 gsave 10 dict begin
-495 45 44 18 ellipse_path
+381 18 44 18 ellipse_path
 stroke
 gsave 10 dict begin
-495 46 moveto (Type_errors) 68 14.00 -0.50 alignedtext
+381 19 moveto (Type_errors) 68 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Typeops -> Type_errors
-newpath 299 66 moveto
-337 62 399 55 443 51 curveto
-stroke
-newpath 442 49 moveto
-452 50 lineto
-442 54 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Closure
-gsave 10 dict begin
-495 99 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-495 100 moveto (Closure) 43 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Reduction -> Closure
-newpath 414 98 moveto
-427 98 441 98 453 98 curveto
-stroke
-newpath 453 96 moveto
-463 98 lineto
-453 101 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Environ
-gsave 10 dict begin
-815 72 33 18 ellipse_path
+newpath 297 38 moveto
+308 36 321 33 333 30 curveto
 stroke
-gsave 10 dict begin
-815 73 moveto (Environ) 45 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Type_errors -> Environ
-newpath 539 49 moveto
-601 54 713 63 774 68 curveto
-stroke
-newpath 772 65 moveto
-782 69 lineto
-772 70 lineto
+newpath 332 28 moveto
+342 27 lineto
+333 33 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Inductive
+%	Reduction
 gsave 10 dict begin
-927 126 36 18 ellipse_path
+501 45 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-927 127 moveto (Inductive) 52 14.00 -0.50 alignedtext
+501 46 moveto (Reduction) 57 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Environ -> Inductive
-newpath 840 84 moveto
-855 92 875 101 892 109 curveto
+%	Inductive -> Reduction
+newpath 414 64 moveto
+427 61 442 58 456 55 curveto
 stroke
-newpath 893 107 moveto
-901 113 lineto
-891 111 lineto
+newpath 456 53 moveto
+466 53 lineto
+457 57 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Abstraction
-gsave 10 dict begin
-927 18 43 18 ellipse_path
+%	Type_errors -> Reduction
+newpath 420 27 moveto
+432 29 444 32 456 35 curveto
 stroke
-gsave 10 dict begin
-927 19 moveto (Abstraction) 65 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Environ -> Abstraction
-newpath 840 60 moveto
-854 53 874 44 890 36 curveto
-stroke
-newpath 889 34 moveto
-899 32 lineto
-891 38 lineto
+newpath 456 32 moveto
+465 37 lineto
+455 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Constant
+%	Closure
 gsave 10 dict begin
-927 72 35 18 ellipse_path
+608 45 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-927 73 moveto (Constant) 49 14.00 -0.50 alignedtext
+608 46 moveto (Closure) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Environ -> Constant
-newpath 848 72 moveto
-859 72 871 72 882 72 curveto
+%	Reduction -> Closure
+newpath 540 45 moveto
+549 45 558 45 566 45 curveto
 stroke
-newpath 882 70 moveto
-892 72 lineto
-882 75 lineto
+newpath 566 43 moveto
+576 45 lineto
+566 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Term
 gsave 10 dict begin
-1125 45 27 18 ellipse_path
+1229 45 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1125 46 moveto (Term) 30 14.00 -0.50 alignedtext
+1229 46 moveto (Term) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Univ
-newpath 1150 52 moveto
-1161 55 1175 59 1187 62 curveto
-stroke
-newpath 1187 59 moveto
-1196 65 lineto
-1186 64 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Generic
-gsave 10 dict begin
-1221 18 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-1221 19 moveto (Generic) 44 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Term -> Generic
-newpath 1150 38 moveto
-1160 35 1171 32 1182 29 curveto
-stroke
-newpath 1182 26 moveto
-1192 26 lineto
-1183 31 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Generic -> Names
-newpath 1250 26 moveto
-1260 29 1273 32 1284 35 curveto
-stroke
-newpath 1284 32 moveto
-1293 38 lineto
-1283 37 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Sosub
-gsave 10 dict begin
-1034 18 27 18 ellipse_path
+newpath 1256 45 moveto
+1264 45 1273 45 1282 45 curveto
 stroke
-gsave 10 dict begin
-1034 19 moveto (Sosub) 34 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Sosub -> Term
-newpath 1059 26 moveto
-1069 29 1080 32 1091 35 curveto
-stroke
-newpath 1091 32 moveto
-1100 38 lineto
-1090 37 lineto
+newpath 1282 43 moveto
+1292 45 lineto
+1282 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sign
 gsave 10 dict begin
-1034 72 27 18 ellipse_path
+1139 45 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1034 73 moveto (Sign) 25 14.00 -0.50 alignedtext
+1139 46 moveto (Sign) 25 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sign -> Term
-newpath 1059 65 moveto
-1069 62 1080 58 1091 55 curveto
+newpath 1166 45 moveto
+1174 45 1183 45 1192 45 curveto
 stroke
-newpath 1090 53 moveto
-1100 53 lineto
-1091 58 lineto
+newpath 1192 43 moveto
+1202 45 lineto
+1192 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Safe_typing
 gsave 10 dict begin
-44 70 44 18 ellipse_path
+44 45 44 18 ellipse_path
 stroke
 gsave 10 dict begin
-44 71 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
+44 46 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Indtypes
 gsave 10 dict begin
-159 70 34 18 ellipse_path
+159 45 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-159 71 moveto (Indtypes) 48 14.00 -0.50 alignedtext
+159 46 moveto (Indtypes) 48 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Safe_typing -> Indtypes
-newpath 88 70 moveto
-97 70 106 70 114 70 curveto
+newpath 88 45 moveto
+97 45 106 45 114 45 curveto
 stroke
-newpath 114 68 moveto
-124 70 lineto
-114 73 lineto
+newpath 114 43 moveto
+124 45 lineto
+114 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Indtypes -> Typeops
-newpath 194 70 moveto
-203 70 212 70 220 70 curveto
+newpath 194 45 moveto
+203 45 212 45 220 45 curveto
 stroke
-newpath 220 68 moveto
-230 70 lineto
-220 73 lineto
+newpath 220 43 moveto
+230 45 lineto
+220 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Instantiate
 gsave 10 dict begin
-616 98 39 18 ellipse_path
+716 45 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-616 99 moveto (Instantiate) 58 14.00 -0.50 alignedtext
+716 46 moveto (Instantiate) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Closure -> Instantiate
-newpath 527 99 moveto
-539 99 553 98 566 98 curveto
+newpath 640 45 moveto
+648 45 657 45 666 45 curveto
 stroke
-newpath 566 96 moveto
-576 98 lineto
-566 101 lineto
+newpath 666 43 moveto
+676 45 lineto
+666 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evd
 gsave 10 dict begin
-719 96 27 18 ellipse_path
+819 45 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-719 97 moveto (Evd) 22 14.00 -0.50 alignedtext
+819 46 moveto (Evd) 22 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Instantiate -> Evd
-newpath 656 97 moveto
-665 97 674 97 682 97 curveto
+newpath 756 45 moveto
+765 45 774 45 782 45 curveto
 stroke
-newpath 682 95 moveto
-692 97 lineto
-682 100 lineto
+newpath 782 43 moveto
+792 45 lineto
+782 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
+%	Environ
+gsave 10 dict begin
+915 45 33 18 ellipse_path
+stroke
+gsave 10 dict begin
+915 46 moveto (Environ) 45 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
 %	Evd -> Environ
-newpath 744 90 moveto
-754 88 765 85 775 82 curveto
+newpath 846 45 moveto
+854 45 863 45 872 45 curveto
 stroke
-newpath 775 80 moveto
-785 80 lineto
-776 84 lineto
+newpath 872 43 moveto
+882 45 lineto
+872 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Inductive -> Sign
-newpath 953 113 moveto
-968 105 988 96 1004 87 curveto
+%	Declarations
+gsave 10 dict begin
+1030 45 45 18 ellipse_path
 stroke
-newpath 1002 85 moveto
-1012 83 lineto
-1004 90 lineto
-closepath
-gsave 0 setgray stroke grestore fill
+gsave 10 dict begin
+1030 46 moveto (Declarations) 70 14.00 -0.50 alignedtext
+end grestore
+end grestore
 
-%	Abstraction -> Sosub
-newpath 970 18 moveto
-979 18 988 18 996 18 curveto
+%	Environ -> Declarations
+newpath 948 45 moveto
+956 45 965 45 974 45 curveto
 stroke
-newpath 996 16 moveto
-1006 18 lineto
-996 21 lineto
+newpath 974 43 moveto
+984 45 lineto
+974 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Constant -> Sign
-newpath 962 72 moveto
-974 72 986 72 997 72 curveto
+%	Declarations -> Sign
+newpath 1076 45 moveto
+1085 45 1094 45 1102 45 curveto
 stroke
-newpath 997 70 moveto
-1007 72 lineto
-997 75 lineto
+newpath 1102 43 moveto
+1112 45 lineto
+1102 48 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index a6a5fc38d..f8995d649 100644
--- a/doc/library.dep.ps
+++ b/doc/library.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jc) Jean-Christophe,,,,
+%%For: (jacek) Jacek Chrzaszcz
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 429 419
+%%BoundingBox: 36 36 519 295
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(() show i str cvs show (,) show j str cvs show ()) show
+			(\() show i str cvs show (,) show j str cvs show (\)) show
 		grestore
 	} if
 } bind def
@@ -139,9 +139,9 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 429 419
+%%PageBoundingBox: 36 36 519 295
 gsave
-35 35 394 384 boxprim clip newpath
+35 35 484 260 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
 0 0 translate 0 rotate
@@ -150,252 +150,233 @@ gsave
 
 %	States
 gsave 10 dict begin
-136 364 27 18 ellipse_path
+27 217 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 365 moveto (States) 33 14.00 -0.50 alignedtext
+27 218 moveto (States) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Lib
+%	Library
 gsave 10 dict begin
-244 264 27 18 ellipse_path
+122 217 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-244 265 moveto (Lib) 19 14.00 -0.50 alignedtext
+122 218 moveto (Library) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	States -> Lib
-newpath 156 352 moveto
-162 348 168 343 172 340 curveto
-187 326 208 303 224 286 curveto
+%	States -> Library
+newpath 54 217 moveto
+62 217 72 217 81 217 curveto
 stroke
-newpath 222 285 moveto
-230 279 lineto
-225 288 lineto
+newpath 81 215 moveto
+91 217 lineto
+81 220 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Summary
+%	Global
 gsave 10 dict begin
-354 164 37 18 ellipse_path
+334 93 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-354 165 moveto (Summary) 54 14.00 -0.50 alignedtext
+334 94 moveto (Global) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Lib -> Summary
-newpath 260 249 moveto
-279 232 308 205 329 186 curveto
+%	Library -> Global
+newpath 145 205 moveto
+176 188 231 158 262 140 curveto
+274 132 291 121 306 112 curveto
 stroke
-newpath 327 185 moveto
-336 180 lineto
-330 188 lineto
+newpath 305 110 moveto
+314 106 lineto
+308 114 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Libobject
+%	Goptions
 gsave 10 dict begin
-354 264 37 18 ellipse_path
+226 240 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-354 265 moveto (Libobject) 53 14.00 -0.50 alignedtext
+226 241 moveto (Goptions) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Lib -> Libobject
-newpath 271 264 moveto
-282 264 295 264 307 264 curveto
+%	Library -> Goptions
+newpath 151 223 moveto
+161 225 172 228 183 230 curveto
 stroke
-newpath 307 262 moveto
-317 264 lineto
-307 267 lineto
+newpath 184 228 moveto
+193 232 lineto
+183 232 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Redinfo
+%	Nametab
 gsave 10 dict begin
-136 164 33 18 ellipse_path
+334 20 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 165 moveto (Redinfo) 45 14.00 -0.50 alignedtext
+334 21 moveto (Nametab) 50 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Global
+%	Summary
 gsave 10 dict begin
-244 164 29 18 ellipse_path
+444 93 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-244 165 moveto (Global) 38 14.00 -0.50 alignedtext
+444 94 moveto (Summary) 54 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Redinfo -> Global
-newpath 169 164 moveto
-180 164 193 164 204 164 curveto
+%	Nametab -> Summary
+newpath 356 34 moveto
+373 45 395 61 414 73 curveto
 stroke
-newpath 204 162 moveto
-214 164 lineto
-204 167 lineto
+newpath 415 71 moveto
+422 78 lineto
+412 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Global -> Summary
-newpath 274 164 moveto
-284 164 295 164 306 164 curveto
-stroke
-newpath 306 162 moveto
-316 164 lineto
-306 167 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Nametab
-gsave 10 dict begin
-244 87 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-244 88 moveto (Nametab) 50 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Nametab -> Summary
-newpath 265 102 moveto
-282 113 306 130 325 144 curveto
+newpath 364 93 moveto
+374 93 385 93 396 93 curveto
 stroke
-newpath 326 142 moveto
-333 149 lineto
-323 146 lineto
+newpath 396 91 moveto
+406 93 lineto
+396 96 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Library
+%	Lib
 gsave 10 dict begin
-136 218 31 18 ellipse_path
+334 156 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 219 moveto (Library) 41 14.00 -0.50 alignedtext
+334 157 moveto (Lib) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Library -> Lib
-newpath 161 229 moveto
-176 235 196 244 212 251 curveto
+%	Goptions -> Lib
+newpath 246 225 moveto
+264 211 290 190 309 175 curveto
 stroke
-newpath 212 248 moveto
-221 254 lineto
-211 253 lineto
+newpath 306 174 moveto
+316 170 lineto
+309 178 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Library -> Global
-newpath 160 206 moveto
-175 198 196 188 213 179 curveto
+%	Lib -> Summary
+newpath 355 144 moveto
+371 135 393 122 412 112 curveto
 stroke
-newpath 211 177 moveto
-221 175 lineto
-213 182 lineto
+newpath 410 110 moveto
+420 107 lineto
+413 114 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Impargs
+%	Libobject
 gsave 10 dict begin
-136 110 33 18 ellipse_path
+444 156 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 111 moveto (Impargs) 45 14.00 -0.50 alignedtext
+444 157 moveto (Libobject) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Impargs -> Global
-newpath 161 122 moveto
-176 130 196 140 213 148 curveto
+%	Lib -> Libobject
+newpath 361 156 moveto
+372 156 385 156 397 156 curveto
 stroke
-newpath 213 145 moveto
-221 152 lineto
-211 150 lineto
+newpath 397 154 moveto
+407 156 lineto
+397 159 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Goptions
+%	Impargs
 gsave 10 dict begin
-136 310 36 18 ellipse_path
+226 56 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 311 moveto (Goptions) 51 14.00 -0.50 alignedtext
+226 57 moveto (Impargs) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Goptions -> Lib
-newpath 164 298 moveto
-179 292 197 284 212 278 curveto
+%	Impargs -> Global
+newpath 254 66 moveto
+268 71 285 77 299 81 curveto
 stroke
-newpath 211 276 moveto
-221 274 lineto
-213 280 lineto
+newpath 299 78 moveto
+308 84 lineto
+298 83 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declare
 gsave 10 dict begin
-32 87 32 18 ellipse_path
+122 83 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-32 88 moveto (Declare) 43 14.00 -0.50 alignedtext
+122 84 moveto (Declare) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Declare -> Lib
-newpath 36 105 moveto
-44 140 66 219 100 248 curveto
-123 266 172 268 206 267 curveto
+%	Declare -> Nametab
+newpath 137 67 moveto
+151 52 173 32 190 26 curveto
+217 19 260 18 291 18 curveto
 stroke
-newpath 207 264 moveto
-217 266 lineto
-207 269 lineto
+newpath 288 16 moveto
+298 18 lineto
+288 21 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Declare -> Nametab
-newpath 64 84 moveto
-76 82 90 81 100 80 curveto
-126 79 168 81 199 83 curveto
+%	Declare -> Lib
+newpath 137 99 moveto
+151 114 173 134 190 140 curveto
+219 149 267 153 300 155 curveto
 stroke
-newpath 199 81 moveto
-209 84 lineto
-199 85 lineto
+newpath 297 153 moveto
+307 155 lineto
+297 158 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declare -> Impargs
-newpath 62 94 moveto
-73 96 85 99 96 101 curveto
+newpath 151 75 moveto
+162 72 175 69 187 66 curveto
 stroke
-newpath 96 98 moveto
-105 103 lineto
-95 103 lineto
+newpath 186 64 moveto
+196 64 lineto
+187 69 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Indrec
 gsave 10 dict begin
-136 18 28 18 ellipse_path
+226 110 28 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 19 moveto (Indrec) 35 14.00 -0.50 alignedtext
+226 111 moveto (Indrec) 35 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Declare -> Indrec
-newpath 53 73 moveto
-69 63 91 48 108 36 curveto
+newpath 151 91 moveto
+163 94 178 98 191 101 curveto
 stroke
-newpath 106 34 moveto
-116 31 lineto
-109 38 lineto
+newpath 191 98 moveto
+200 103 lineto
+190 103 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index de816c0af..97d69aa0d 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jc) Jean-Christophe,,,,
+%%For: (jacek) Jacek Chrzaszcz
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 183
+%%BoundingBox: 36 36 577 217
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(() show i str cvs show (,) show j str cvs show ()) show
+			(\() show i str cvs show (,) show j str cvs show (\)) show
 		grestore
 	} if
 } bind def
@@ -139,283 +139,314 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 183
+%%PageBoundingBox: 36 36 577 217
 gsave
-35 35 541 148 boxprim clip newpath
+35 35 542 182 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.7988 set_scale
+0.8060 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
-%	Termast
+%	Pcoq
 gsave 10 dict begin
-367 160 33 18 ellipse_path
+547 110 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-367 161 moveto (Termast) 45 14.00 -0.50 alignedtext
+547 111 moveto (Pcoq) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Ast
+%	Coqast
 gsave 10 dict begin
-463 83 27 18 ellipse_path
+640 110 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-463 84 moveto (Ast) 19 14.00 -0.50 alignedtext
+640 111 moveto (Coqast) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Termast -> Ast
-newpath 386 145 moveto
-401 133 422 116 438 103 curveto
+%	Pcoq -> Coqast
+newpath 574 110 moveto
+582 110 591 110 600 110 curveto
 stroke
-newpath 436 102 moveto
-445 97 lineto
-439 105 lineto
+newpath 600 108 moveto
+610 110 lineto
+600 113 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Pcoq
+%	Extend
 gsave 10 dict begin
-553 83 27 18 ellipse_path
+364 110 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-553 84 moveto (Pcoq) 28 14.00 -0.50 alignedtext
+364 111 moveto (Extend) 39 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Ast -> Pcoq
-newpath 490 83 moveto
-498 83 507 83 516 83 curveto
-stroke
-newpath 516 81 moveto
-526 83 lineto
-516 86 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Printer
+%	Ast
 gsave 10 dict begin
-136 166 29 18 ellipse_path
+457 110 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 167 moveto (Printer) 38 14.00 -0.50 alignedtext
+457 111 moveto (Ast) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Printer -> Termast
-newpath 166 165 moveto
-206 164 278 162 325 161 curveto
+%	Extend -> Ast
+newpath 394 110 moveto
+402 110 411 110 420 110 curveto
 stroke
-newpath 324 159 moveto
-334 161 lineto
-324 164 lineto
+newpath 420 108 moveto
+430 110 lineto
+420 113 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Esyntax
+%	Ast -> Pcoq
+newpath 484 110 moveto
+492 110 501 110 510 110 curveto
+stroke
+newpath 510 108 moveto
+520 110 lineto
+510 113 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Termast
 gsave 10 dict begin
-258 126 33 18 ellipse_path
+258 44 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-258 127 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+258 45 moveto (Termast) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Printer -> Esyntax
-newpath 162 157 moveto
-179 152 202 144 221 138 curveto
+%	Termast -> Ast
+newpath 285 34 moveto
+317 23 369 9 394 26 curveto
+411 38 430 65 442 85 curveto
 stroke
-newpath 220 136 moveto
-230 135 lineto
-221 141 lineto
+newpath 444 83 moveto
+447 93 lineto
+440 86 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Extend
+%	Pattern
 gsave 10 dict begin
-367 83 30 18 ellipse_path
+364 56 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-367 84 moveto (Extend) 39 14.00 -0.50 alignedtext
+364 57 moveto (Pattern) 39 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Esyntax -> Extend
-newpath 285 115 moveto
-299 110 318 103 333 97 curveto
+%	Termast -> Pattern
+newpath 290 48 moveto
+301 49 313 50 325 52 curveto
 stroke
-newpath 332 95 moveto
-342 93 lineto
-334 99 lineto
+newpath 324 49 moveto
+334 53 lineto
+324 54 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Pretty
+%	Printer
 gsave 10 dict begin
-27 166 27 18 ellipse_path
+136 44 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-27 167 moveto (Pretty) 33 14.00 -0.50 alignedtext
+136 45 moveto (Printer) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pretty -> Printer
-newpath 54 166 moveto
-67 166 82 166 96 166 curveto
+%	Printer -> Termast
+newpath 166 44 moveto
+181 44 199 44 215 44 curveto
 stroke
-newpath 96 164 moveto
-106 166 lineto
-96 169 lineto
+newpath 215 42 moveto
+225 44 lineto
+215 47 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Coqast
+%	Esyntax
 gsave 10 dict begin
-646 110 30 18 ellipse_path
+258 98 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-646 111 moveto (Coqast) 38 14.00 -0.50 alignedtext
+258 99 moveto (Esyntax) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pcoq -> Coqast
-newpath 578 90 moveto
-587 93 599 96 609 99 curveto
+%	Printer -> Esyntax
+newpath 160 55 moveto
+178 63 204 74 224 83 curveto
 stroke
-newpath 610 97 moveto
-619 102 lineto
-609 102 lineto
+newpath 224 80 moveto
+232 87 lineto
+222 85 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Lexer
+%	Esyntax -> Extend
+newpath 290 102 moveto
+301 103 313 104 325 106 curveto
+stroke
+newpath 324 103 moveto
+334 107 lineto
+324 108 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Pretty
 gsave 10 dict begin
-646 56 27 18 ellipse_path
+27 44 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-646 57 moveto (Lexer) 32 14.00 -0.50 alignedtext
+27 45 moveto (Pretty) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pcoq -> Lexer
-newpath 578 76 moveto
-588 73 601 69 612 66 curveto
+%	Pretty -> Printer
+newpath 54 44 moveto
+67 44 82 44 96 44 curveto
 stroke
-newpath 611 64 moveto
-621 63 lineto
-612 69 lineto
+newpath 96 42 moveto
+106 44 lineto
+96 47 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_zsyntax
 gsave 10 dict begin
-136 24 40 18 ellipse_path
+136 152 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 25 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
+136 153 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_zsyntax -> Esyntax
-newpath 158 39 moveto
-167 46 176 53 182 59 curveto
-196 72 204 90 218 102 curveto
-220 104 222 106 225 108 curveto
+newpath 165 139 moveto
+182 131 206 121 224 113 curveto
 stroke
-newpath 226 106 moveto
-234 113 lineto
-224 110 lineto
+newpath 222 111 moveto
+232 109 lineto
+224 116 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Astterm
 gsave 10 dict begin
-258 18 33 18 ellipse_path
+258 152 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-258 19 moveto (Astterm) 45 14.00 -0.50 alignedtext
+258 153 moveto (Astterm) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_zsyntax -> Astterm
-newpath 176 22 moveto
-189 21 203 20 215 20 curveto
+newpath 176 152 moveto
+189 152 203 152 215 152 curveto
 stroke
-newpath 215 18 moveto
-225 20 lineto
-215 23 lineto
+newpath 215 150 moveto
+225 152 lineto
+215 155 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Astterm -> Ast
-newpath 289 25 moveto
-321 32 371 44 400 53 curveto
-409 56 421 62 433 67 curveto
+newpath 291 150 moveto
+322 149 367 146 394 140 curveto
+394 140 411 132 427 124 curveto
+stroke
+newpath 425 122 moveto
+435 120 lineto
+427 127 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Astterm -> Pattern
+newpath 282 139 moveto
+288 136 294 132 298 128 curveto
+313 114 321 94 334 80 curveto
+334 80 336 79 339 77 curveto
 stroke
-newpath 434 65 moveto
-442 72 lineto
-432 69 lineto
+newpath 337 76 moveto
+346 71 lineto
+340 79 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax
 gsave 10 dict begin
-136 89 45 18 ellipse_path
+136 98 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 90 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
+136 99 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_natsyntax -> Esyntax
-newpath 172 100 moveto
-187 105 205 110 220 114 curveto
+newpath 182 98 moveto
+193 98 205 98 216 98 curveto
 stroke
-newpath 220 111 moveto
-229 117 lineto
-219 116 lineto
+newpath 215 96 moveto
+225 98 lineto
+215 101 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax -> Astterm
-newpath 162 74 moveto
-181 63 207 47 227 35 curveto
+newpath 166 111 moveto
+184 119 206 129 224 137 curveto
 stroke
-newpath 225 33 moveto
-235 31 lineto
-227 38 lineto
+newpath 224 134 moveto
+233 140 lineto
+223 139 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Extend -> Ast
-newpath 397 83 moveto
-406 83 417 83 426 83 curveto
+%	Egrammar
+gsave 10 dict begin
+258 206 40 18 ellipse_path
 stroke
-newpath 426 81 moveto
-436 83 lineto
-426 86 lineto
+gsave 10 dict begin
+258 207 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Egrammar -> Extend
+newpath 284 192 moveto
+289 189 295 185 298 182 curveto
+312 170 330 149 344 133 curveto
+stroke
+newpath 342 132 moveto
+350 126 lineto
+345 135 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Egrammar
+%	Lexer
 gsave 10 dict begin
-258 72 40 18 ellipse_path
+364 206 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-258 73 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+364 207 moveto (Lexer) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Egrammar -> Extend
-newpath 297 76 moveto
-307 77 318 78 328 79 curveto
+%	Egrammar -> Lexer
+newpath 298 206 moveto
+308 206 318 206 327 206 curveto
 stroke
-newpath 327 76 moveto
-337 80 lineto
-327 81 lineto
+newpath 327 204 moveto
+337 206 lineto
+327 209 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index 6a06d166f..9e5348ac4 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jc) Jean-Christophe,,,,
+%%For: (jacek) Jacek Chrzaszcz
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 199
+%%BoundingBox: 36 36 577 188
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(() show i str cvs show (,) show j str cvs show ()) show
+			(\() show i str cvs show (,) show j str cvs show (\)) show
 		grestore
 	} if
 } bind def
@@ -139,293 +139,332 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 199
+%%PageBoundingBox: 36 36 577 188
 gsave
-35 35 541 164 boxprim clip newpath
+35 35 542 153 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.8207 set_scale
+0.6308 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Multcase
 gsave 10 dict begin
-257 72 36 18 ellipse_path
+347 70 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-257 73 moveto (Multcase) 51 14.00 -0.50 alignedtext
+347 71 moveto (Multcase) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Evarutil
 gsave 10 dict begin
-370 72 33 18 ellipse_path
+460 72 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-370 73 moveto (Evarutil) 45 14.00 -0.50 alignedtext
+460 73 moveto (Evarutil) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Multcase -> Evarutil
-newpath 293 72 moveto
-304 72 316 72 327 72 curveto
+newpath 383 71 moveto
+394 71 406 71 417 71 curveto
 stroke
-newpath 327 70 moveto
-337 72 lineto
-327 75 lineto
+newpath 417 69 moveto
+427 71 lineto
+417 74 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pretype_errors
 gsave 10 dict begin
-498 45 51 18 ellipse_path
+588 72 51 18 ellipse_path
 stroke
 gsave 10 dict begin
-498 46 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
+588 73 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Evarutil -> Pretype_errors
-newpath 401 65 moveto
-414 63 429 59 443 56 curveto
+newpath 493 72 moveto
+503 72 515 72 526 72 curveto
 stroke
-newpath 443 54 moveto
-453 54 lineto
-444 58 lineto
+newpath 526 70 moveto
+536 72 lineto
+526 75 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Tacred
+gsave 10 dict begin
+712 180 29 18 ellipse_path
+stroke
+gsave 10 dict begin
+712 181 moveto (Tacred) 38 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Retyping
+gsave 10 dict begin
+820 180 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+820 181 moveto (Retyping) 51 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Tacred -> Retyping
+newpath 742 180 moveto
+752 180 763 180 774 180 curveto
+stroke
+newpath 774 178 moveto
+784 180 lineto
+774 183 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Syntax_def
 gsave 10 dict begin
-498 99 42 18 ellipse_path
+588 126 42 18 ellipse_path
 stroke
 gsave 10 dict begin
-498 100 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
+588 127 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Rawterm
 gsave 10 dict begin
-622 72 36 18 ellipse_path
+712 99 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-622 73 moveto (Rawterm) 51 14.00 -0.50 alignedtext
+712 100 moveto (Rawterm) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Syntax_def -> Rawterm
-newpath 536 91 moveto
-550 88 565 84 579 81 curveto
+newpath 626 118 moveto
+640 115 655 111 669 108 curveto
 stroke
-newpath 579 79 moveto
-589 79 lineto
-580 83 lineto
+newpath 669 106 moveto
+679 106 lineto
+670 110 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Recordops
 gsave 10 dict begin
-370 126 40 18 ellipse_path
+460 222 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-370 127 moveto (Recordops) 59 14.00 -0.50 alignedtext
+460 223 moveto (Recordops) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Classops
 gsave 10 dict begin
-498 153 35 18 ellipse_path
+588 180 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-498 154 moveto (Classops) 49 14.00 -0.50 alignedtext
+588 181 moveto (Classops) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Recordops -> Classops
-newpath 406 134 moveto
-422 137 440 141 456 144 curveto
+newpath 493 211 moveto
+510 206 532 199 549 193 curveto
 stroke
-newpath 456 141 moveto
-465 146 lineto
-455 146 lineto
+newpath 548 191 moveto
+558 190 lineto
+549 196 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Tacred
-gsave 10 dict begin
-622 153 29 18 ellipse_path
+%	Classops -> Tacred
+newpath 623 180 moveto
+639 180 657 180 673 180 curveto
 stroke
-gsave 10 dict begin
-622 154 moveto (Tacred) 38 14.00 -0.50 alignedtext
-end grestore
-end grestore
+newpath 672 178 moveto
+682 180 lineto
+672 183 lineto
+closepath
+gsave 0 setgray stroke grestore fill
 
-%	Classops -> Tacred
-newpath 533 153 moveto
-549 153 567 153 583 153 curveto
+%	Classops -> Rawterm
+newpath 615 169 moveto
+625 165 634 160 640 156 curveto
+654 147 672 133 687 121 curveto
 stroke
-newpath 582 151 moveto
-592 153 lineto
-582 156 lineto
+newpath 685 120 moveto
+694 115 lineto
+688 123 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pretyping
 gsave 10 dict begin
-38 72 37 18 ellipse_path
+38 178 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-38 73 moveto (Pretyping) 54 14.00 -0.50 alignedtext
+38 179 moveto (Pretyping) 54 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Cases
 gsave 10 dict begin
-148 99 27 18 ellipse_path
+139 178 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-148 100 moveto (Cases) 32 14.00 -0.50 alignedtext
+139 179 moveto (Cases) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pretyping -> Cases
-newpath 72 80 moveto
-85 83 101 87 114 91 curveto
+newpath 76 178 moveto
+85 178 94 178 102 178 curveto
 stroke
-newpath 114 88 moveto
-123 93 lineto
-113 93 lineto
+newpath 102 176 moveto
+112 178 lineto
+102 181 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coercion
 gsave 10 dict begin
-148 45 36 18 ellipse_path
+238 178 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-148 46 moveto (Coercion) 51 14.00 -0.50 alignedtext
+238 179 moveto (Coercion) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pretyping -> Coercion
-newpath 72 64 moveto
-83 62 95 59 106 56 curveto
+%	Cases -> Coercion
+newpath 166 178 moveto
+174 178 183 178 192 178 curveto
 stroke
-newpath 105 54 moveto
-115 53 lineto
-106 59 lineto
+newpath 192 176 moveto
+202 178 lineto
+192 181 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evarconv
-gsave 10 dict begin
-257 126 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-257 127 moveto (Evarconv) 53 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Cases -> Evarconv
-newpath 174 105 moveto
-186 108 201 112 214 116 curveto
+%	Pretype_errors -> Rawterm
+newpath 632 82 moveto
+644 84 657 87 669 90 curveto
 stroke
-newpath 215 114 moveto
-224 118 lineto
-214 118 lineto
+newpath 670 88 moveto
+679 92 lineto
+669 92 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Retyping
+%	Evarconv
 gsave 10 dict begin
-257 18 36 18 ellipse_path
+347 178 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-257 19 moveto (Retyping) 51 14.00 -0.50 alignedtext
+347 179 moveto (Evarconv) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Cases -> Retyping
-newpath 167 86 moveto
-174 82 180 78 184 75 curveto
-197 64 208 52 220 42 curveto
-222 40 225 38 228 36 curveto
+%	Evarconv -> Evarutil
+newpath 371 164 moveto
+376 161 381 157 384 154 curveto
+400 140 423 114 440 95 curveto
 stroke
-newpath 224 35 moveto
-234 32 lineto
-227 40 lineto
+newpath 437 94 moveto
+446 89 lineto
+441 98 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Coercion -> Evarconv
-newpath 170 59 moveto
-176 63 180 66 184 69 curveto
-197 79 208 91 220 102 curveto
-222 104 225 106 228 108 curveto
-stroke
-newpath 227 104 moveto
-234 112 lineto
-224 109 lineto
+%	Evarconv -> Recordops
+newpath 376 189 moveto
+390 194 406 200 421 206 curveto
+stroke
+newpath 422 204 moveto
+430 210 lineto
+420 208 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Coercion -> Retyping
-newpath 180 37 moveto
-191 35 204 31 216 28 curveto
+%	Typing
+gsave 10 dict begin
+460 168 30 18 ellipse_path
 stroke
-newpath 215 26 moveto
-225 26 lineto
-216 31 lineto
-closepath
-gsave 0 setgray stroke grestore fill
+gsave 10 dict begin
+460 169 moveto (Typing) 40 14.00 -0.50 alignedtext
+end grestore
+end grestore
 
-%	Pretype_errors -> Rawterm
-newpath 542 55 moveto
-554 57 567 60 579 63 curveto
+%	Evarconv -> Typing
+newpath 384 175 moveto
+396 174 409 173 421 172 curveto
 stroke
-newpath 580 61 moveto
-589 65 lineto
-579 65 lineto
+newpath 420 170 moveto
+430 171 lineto
+420 175 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evarconv -> Evarutil
-newpath 283 113 moveto
-299 105 320 95 337 88 curveto
+%	Detyping
+gsave 10 dict begin
+588 18 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+588 19 moveto (Detyping) 52 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Detyping -> Rawterm
+newpath 616 30 moveto
+625 34 634 38 640 42 curveto
+653 51 671 65 687 77 curveto
 stroke
-newpath 335 86 moveto
-345 84 lineto
-337 91 lineto
+newpath 688 75 moveto
+694 83 lineto
+685 78 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evarconv -> Recordops
-newpath 294 126 moveto
-302 126 311 126 320 126 curveto
+%	Coercion -> Evarconv
+newpath 274 178 moveto
+282 178 291 178 300 178 curveto
 stroke
-newpath 320 124 moveto
-330 126 lineto
-320 129 lineto
+newpath 300 176 moveto
+310 178 lineto
+300 181 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Typing
+%	Class
 gsave 10 dict begin
-370 180 30 18 ellipse_path
+347 124 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-370 181 moveto (Typing) 40 14.00 -0.50 alignedtext
+347 125 moveto (Class) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Evarconv -> Typing
-newpath 283 139 moveto
-299 147 321 157 338 165 curveto
+%	Class -> Classops
+newpath 374 126 moveto
+408 128 466 133 500 138 curveto
+514 141 524 150 536 156 curveto
+541 158 549 162 556 165 curveto
+stroke
+newpath 554 161 moveto
+562 168 lineto
+552 166 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Class -> Typing
+newpath 370 133 moveto
+386 139 408 147 425 154 curveto
 stroke
-newpath 338 162 moveto
-346 169 lineto
-336 167 lineto
+newpath 426 152 moveto
+434 158 lineto
+424 156 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index 9f92d1e95..b8f9a065e 100644
--- a/doc/proofs.dep.ps
+++ b/doc/proofs.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jc) Jean-Christophe,,,,
+%%For: (jacek) Jacek Chrzaszcz
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 145
+%%BoundingBox: 36 36 577 129
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(() show i str cvs show (,) show j str cvs show ()) show
+			(\() show i str cvs show (,) show j str cvs show (\)) show
 		grestore
 	} if
 } bind def
@@ -139,12 +139,12 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 145
+%%PageBoundingBox: 36 36 577 129
 gsave
-35 35 541 110 boxprim clip newpath
+35 35 542 94 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.7521 set_scale
+0.6444 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
@@ -272,6 +272,25 @@ newpath 622 70 moveto
 closepath
 gsave 0 setgray stroke grestore fill
 
+%	Proof_type
+gsave 10 dict begin
+796 72 41 18 ellipse_path
+stroke
+gsave 10 dict begin
+796 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Proof_trees -> Proof_type
+newpath 718 72 moveto
+727 72 736 72 744 72 curveto
+stroke
+newpath 744 70 moveto
+754 72 lineto
+744 75 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
 %	Pfedit
 gsave 10 dict begin
 141 72 27 18 ellipse_path
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index 0ff40bcdc..940e81966 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jc) Jean-Christophe,,,,
+%%For: (jacek) Jacek Chrzaszcz
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 152
+%%BoundingBox: 36 36 577 194
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(() show i str cvs show (,) show j str cvs show ()) show
+			(\() show i str cvs show (,) show j str cvs show (\)) show
 		grestore
 	} if
 } bind def
@@ -139,279 +139,396 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 152
+%%PageBoundingBox: 36 36 577 194
 gsave
-35 35 541 117 boxprim clip newpath
+35 35 542 159 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.7563 set_scale
+0.6618 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Termdn
 gsave 10 dict begin
-462 18 32 18 ellipse_path
+653 202 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-462 19 moveto (Termdn) 44 14.00 -0.50 alignedtext
+653 203 moveto (Termdn) 44 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Dn
 gsave 10 dict begin
-579 18 27 18 ellipse_path
+771 202 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-579 19 moveto (Dn) 17 14.00 -0.50 alignedtext
+771 203 moveto (Dn) 17 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Termdn -> Dn
-newpath 495 18 moveto
-510 18 527 18 543 18 curveto
+newpath 686 202 moveto
+701 202 719 202 735 202 curveto
 stroke
-newpath 542 16 moveto
-552 18 lineto
-542 21 lineto
+newpath 734 200 moveto
+744 202 lineto
+734 205 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Tauto
+gsave 10 dict begin
+127 220 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+127 221 moveto (Tauto) 32 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Auto
+gsave 10 dict begin
+217 166 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+217 167 moveto (Auto) 28 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Tauto -> Auto
+newpath 147 208 moveto
+159 201 175 191 189 183 curveto
+stroke
+newpath 187 181 moveto
+197 178 lineto
+190 185 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Hiddentac
+gsave 10 dict begin
+319 114 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+319 115 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Auto -> Hiddentac
+newpath 239 155 moveto
+252 148 269 140 284 132 curveto
+stroke
+newpath 283 130 moveto
+293 128 lineto
+285 134 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Dhyp
+gsave 10 dict begin
+319 168 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+319 169 moveto (Dhyp) 31 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Auto -> Dhyp
+newpath 244 167 moveto
+256 167 270 167 282 167 curveto
+stroke
+newpath 282 165 moveto
+292 167 lineto
+282 170 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Tactics
 gsave 10 dict begin
-355 91 30 18 ellipse_path
+545 87 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-355 92 moveto (Tactics) 40 14.00 -0.50 alignedtext
+545 88 moveto (Tactics) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tacticals
+%	Hipattern
 gsave 10 dict begin
-462 91 35 18 ellipse_path
+653 114 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-462 92 moveto (Tacticals) 50 14.00 -0.50 alignedtext
+653 115 moveto (Hipattern) 52 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tactics -> Tacticals
-newpath 386 91 moveto
-395 91 406 91 416 91 curveto
+%	Tactics -> Hipattern
+newpath 573 94 moveto
+584 97 598 100 610 104 curveto
 stroke
-newpath 416 89 moveto
-426 91 lineto
-416 94 lineto
+newpath 611 102 moveto
+620 106 lineto
+610 106 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Pattern
+%	Tacticals
 gsave 10 dict begin
-579 135 30 18 ellipse_path
+653 60 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-579 136 moveto (Pattern) 39 14.00 -0.50 alignedtext
+653 61 moveto (Tacticals) 50 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tacticals -> Pattern
-newpath 491 102 moveto
-507 108 528 116 544 122 curveto
+%	Tactics -> Tacticals
+newpath 573 80 moveto
+585 77 599 74 612 70 curveto
 stroke
-newpath 544 119 moveto
-553 125 lineto
-543 124 lineto
+newpath 611 68 moveto
+621 68 lineto
+612 73 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Wcclausenv
 gsave 10 dict begin
-579 81 44 18 ellipse_path
+771 60 44 18 ellipse_path
 stroke
 gsave 10 dict begin
-579 82 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
+771 61 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacticals -> Wcclausenv
-newpath 497 88 moveto
-506 87 516 87 525 86 curveto
+newpath 689 60 moveto
+698 60 707 60 716 60 curveto
 stroke
-newpath 525 84 moveto
-535 85 lineto
-525 88 lineto
+newpath 716 58 moveto
+726 60 lineto
+716 63 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Stock
+%	Tacentries
 gsave 10 dict begin
-687 135 27 18 ellipse_path
+434 110 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-687 136 moveto (Stock) 31 14.00 -0.50 alignedtext
+434 111 moveto (Tacentries) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pattern -> Stock
-newpath 609 135 moveto
-622 135 637 135 650 135 curveto
+%	Tacentries -> Tactics
+newpath 470 103 moveto
+482 101 495 98 507 95 curveto
 stroke
-newpath 650 133 moveto
-660 135 lineto
-650 138 lineto
+newpath 506 93 moveto
+516 93 lineto
+507 98 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Tacentries
+%	Refine
 gsave 10 dict begin
-244 110 39 18 ellipse_path
+434 18 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-244 111 moveto (Tacentries) 58 14.00 -0.50 alignedtext
+434 19 moveto (Refine) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tacentries -> Tactics
-newpath 281 104 moveto
-293 102 305 99 317 97 curveto
+%	Refine -> Tactics
+newpath 455 31 moveto
+473 42 497 57 516 69 curveto
 stroke
-newpath 316 95 moveto
-326 96 lineto
-316 100 lineto
+newpath 517 67 moveto
+524 74 lineto
+514 71 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Nbtermdn
 gsave 10 dict begin
-244 18 38 18 ellipse_path
+434 202 38 18 ellipse_path
 stroke
 gsave 10 dict begin
-244 19 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
+434 203 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Btermdn
 gsave 10 dict begin
-355 18 35 18 ellipse_path
+545 202 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-355 19 moveto (Btermdn) 49 14.00 -0.50 alignedtext
+545 203 moveto (Btermdn) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Nbtermdn -> Btermdn
-newpath 283 18 moveto
-292 18 301 18 310 18 curveto
+newpath 473 202 moveto
+482 202 491 202 500 202 curveto
 stroke
-newpath 310 16 moveto
-320 18 lineto
-310 21 lineto
+newpath 500 200 moveto
+510 202 lineto
+500 205 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Btermdn -> Termdn
-newpath 390 18 moveto
-400 18 410 18 419 18 curveto
+newpath 580 202 moveto
+590 202 601 202 611 202 curveto
 stroke
-newpath 419 16 moveto
-429 18 lineto
-419 21 lineto
+newpath 610 200 moveto
+620 202 lineto
+610 205 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Hiddentac
+%	Leminv
 gsave 10 dict begin
-129 110 39 18 ellipse_path
+32 112 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-129 111 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
+32 113 moveto (Leminv) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Hiddentac -> Tacentries
-newpath 168 110 moveto
-177 110 186 110 194 110 curveto
+%	Inv
+gsave 10 dict begin
+127 112 27 18 ellipse_path
 stroke
-newpath 194 108 moveto
-204 110 lineto
-194 113 lineto
+gsave 10 dict begin
+127 113 moveto (Inv) 18 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Leminv -> Inv
+newpath 64 112 moveto
+73 112 82 112 90 112 curveto
+stroke
+newpath 90 110 moveto
+100 112 lineto
+90 115 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Inv -> Auto
+newpath 147 124 moveto
+159 131 175 141 189 149 curveto
+stroke
+newpath 190 147 moveto
+197 154 lineto
+187 151 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Elim
 gsave 10 dict begin
-27 110 27 18 ellipse_path
+217 112 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-27 111 moveto (Elim) 27 14.00 -0.50 alignedtext
+217 113 moveto (Elim) 27 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Elim -> Hiddentac
-newpath 54 110 moveto
-62 110 71 110 80 110 curveto
+%	Inv -> Elim
+newpath 154 112 moveto
+162 112 171 112 180 112 curveto
 stroke
-newpath 80 108 moveto
-90 110 lineto
-80 113 lineto
+newpath 180 110 moveto
+190 112 lineto
+180 115 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Dhyp
+%	Equality
 gsave 10 dict begin
-129 56 27 18 ellipse_path
+319 60 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-129 57 moveto (Dhyp) 31 14.00 -0.50 alignedtext
+319 61 moveto (Equality) 47 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Dhyp -> Tactics
-newpath 155 60 moveto
-195 66 270 77 316 85 curveto
+%	Inv -> Equality
+newpath 148 101 moveto
+161 93 178 85 190 82 curveto
+213 76 249 69 277 65 curveto
 stroke
-newpath 315 82 moveto
-325 86 lineto
-315 87 lineto
+newpath 276 63 moveto
+286 64 lineto
+276 68 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Dhyp -> Nbtermdn
-newpath 153 48 moveto
-167 43 187 37 204 31 curveto
+%	Elim -> Hiddentac
+newpath 244 113 moveto
+252 113 261 113 270 113 curveto
 stroke
-newpath 203 29 moveto
-213 28 lineto
-204 34 lineto
+newpath 270 111 moveto
+280 113 lineto
+270 116 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Auto
+%	Equality -> Tactics
+newpath 352 64 moveto
+393 69 463 77 506 82 curveto
+stroke
+newpath 505 79 moveto
+515 83 lineto
+505 84 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Hiddentac -> Tacentries
+newpath 358 113 moveto
+367 112 375 112 384 112 curveto
+stroke
+newpath 384 110 moveto
+394 111 lineto
+384 114 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Eauto
 gsave 10 dict begin
-27 56 27 18 ellipse_path
+127 166 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-27 57 moveto (Auto) 28 14.00 -0.50 alignedtext
+127 167 moveto (Eauto) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Auto -> Hiddentac
-newpath 49 67 moveto
-62 75 80 84 95 92 curveto
+%	Eauto -> Auto
+newpath 154 166 moveto
+162 166 171 166 180 166 curveto
 stroke
-newpath 96 90 moveto
-104 96 lineto
-94 94 lineto
+newpath 180 164 moveto
+190 166 lineto
+180 169 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Auto -> Dhyp
-newpath 54 56 moveto
-66 56 80 56 92 56 curveto
+%	Dhyp -> Tactics
+newpath 346 165 moveto
+380 160 441 152 474 140 curveto
+488 135 507 121 521 108 curveto
+stroke
+newpath 519 107 moveto
+528 102 lineto
+522 110 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Dhyp -> Nbtermdn
+newpath 344 175 moveto
+358 179 376 185 392 189 curveto
 stroke
-newpath 92 54 moveto
-102 56 lineto
-92 59 lineto
+newpath 392 186 moveto
+401 192 lineto
+391 191 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index 28aae6299..a57446d80 100644
--- a/doc/toplevel.dep.ps
+++ b/doc/toplevel.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jc) Jean-Christophe,,,,
+%%For: (jacek) Jacek Chrzaszcz
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 218
+%%BoundingBox: 36 36 577 240
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(() show i str cvs show (,) show j str cvs show ()) show
+			(\() show i str cvs show (,) show j str cvs show (\)) show
 		grestore
 	} if
 } bind def
@@ -139,12 +139,12 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 218
+%%PageBoundingBox: 36 36 577 240
 gsave
-35 35 541 183 boxprim clip newpath
+35 35 542 205 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.5947 set_scale
+0.6683 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
@@ -158,327 +158,321 @@ gsave 10 dict begin
 end grestore
 end grestore
 
+%	Command
+gsave 10 dict begin
+768 96 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+768 97 moveto (Command) 58 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Vernacinterp -> Command
+newpath 675 166 moveto
+681 163 688 159 692 156 curveto
+706 147 725 131 742 118 curveto
+stroke
+newpath 740 117 moveto
+749 112 lineto
+743 120 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
 %	Himsg
 gsave 10 dict begin
-757 205 29 18 ellipse_path
+768 204 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-757 206 moveto (Himsg) 37 14.00 -0.50 alignedtext
+768 205 moveto (Himsg) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp -> Himsg
-newpath 685 189 moveto
-697 191 709 194 721 197 curveto
+newpath 687 188 moveto
+701 190 717 194 731 197 curveto
 stroke
-newpath 721 194 moveto
+newpath 731 194 moveto
+740 199 lineto
 730 199 lineto
-720 199 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Vernacentries
 gsave 10 dict begin
-513 126 49 18 ellipse_path
+513 97 49 18 ellipse_path
 stroke
 gsave 10 dict begin
-513 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
+513 98 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Vernacinterp
-newpath 546 139 moveto
-563 146 586 155 604 163 curveto
+newpath 536 113 moveto
+554 127 581 145 598 156 curveto
+601 158 603 159 607 161 curveto
 stroke
-newpath 605 161 moveto
-613 167 lineto
-603 165 lineto
+newpath 608 159 moveto
+616 166 lineto
+606 163 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Command
+%	Discharge
 gsave 10 dict begin
-645 72 39 18 ellipse_path
+645 126 38 18 ellipse_path
 stroke
 gsave 10 dict begin
-645 73 moveto (Command) 58 14.00 -0.50 alignedtext
+645 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Vernacentries -> Command
-newpath 546 113 moveto
-564 105 588 96 607 88 curveto
+%	Vernacentries -> Discharge
+newpath 555 106 moveto
+570 109 586 113 601 116 curveto
 stroke
-newpath 606 86 moveto
-616 84 lineto
-608 90 lineto
+newpath 601 113 moveto
+610 118 lineto
+600 118 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Discharge
+%	Metasyntax
 gsave 10 dict begin
-645 126 38 18 ellipse_path
+645 72 43 18 ellipse_path
 stroke
 gsave 10 dict begin
-645 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
+645 73 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Vernacentries -> Discharge
-newpath 562 126 moveto
-574 126 585 126 596 126 curveto
+%	Vernacentries -> Metasyntax
+newpath 557 89 moveto
+570 87 583 84 596 81 curveto
 stroke
-newpath 596 124 moveto
-606 126 lineto
-596 129 lineto
+newpath 596 79 moveto
+606 79 lineto
+597 83 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Class
+%	Record
 gsave 10 dict begin
-757 97 27 18 ellipse_path
+645 18 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-757 98 moveto (Class) 30 14.00 -0.50 alignedtext
+645 19 moveto (Record) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Discharge -> Class
-newpath 679 117 moveto
-693 114 709 110 723 106 curveto
+%	Vernacentries -> Record
+newpath 537 81 moveto
+556 69 582 52 598 42 curveto
+602 39 609 36 615 33 curveto
+stroke
+newpath 611 32 moveto
+621 30 lineto
+613 37 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Record -> Command
+newpath 669 29 moveto
+677 34 686 38 692 42 curveto
+706 51 724 63 739 75 curveto
 stroke
-newpath 722 104 moveto
-732 104 lineto
-723 109 lineto
+newpath 741 73 moveto
+747 81 lineto
+738 77 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Vernac
 gsave 10 dict begin
-513 180 30 18 ellipse_path
+513 178 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-513 181 moveto (Vernac) 40 14.00 -0.50 alignedtext
+513 179 moveto (Vernac) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernac -> Vernacinterp
-newpath 544 180 moveto
-557 180 573 180 588 180 curveto
+newpath 544 178 moveto
+557 178 573 179 588 179 curveto
 stroke
-newpath 588 178 moveto
-598 180 lineto
-588 183 lineto
+newpath 588 177 moveto
+598 179 lineto
+588 182 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Toplevel
 gsave 10 dict begin
-239 234 35 18 ellipse_path
+239 232 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-239 235 moveto (Toplevel) 49 14.00 -0.50 alignedtext
+239 233 moveto (Toplevel) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Mltop
 gsave 10 dict begin
-369 261 27 18 ellipse_path
+369 259 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-369 262 moveto (Mltop) 34 14.00 -0.50 alignedtext
+369 260 moveto (Mltop) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Mltop
-newpath 271 241 moveto
-290 245 314 250 334 254 curveto
+newpath 271 239 moveto
+290 243 314 248 334 252 curveto
 stroke
-newpath 334 251 moveto
-343 256 lineto
-333 256 lineto
+newpath 334 249 moveto
+343 254 lineto
+333 254 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Protectedtoplevel
 gsave 10 dict begin
-369 207 59 18 ellipse_path
+369 205 59 18 ellipse_path
 stroke
 gsave 10 dict begin
-369 208 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
+369 206 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Protectedtoplevel
-newpath 271 227 moveto
-283 225 297 222 310 219 curveto
+newpath 271 225 moveto
+283 223 297 220 310 217 curveto
 stroke
-newpath 310 217 moveto
-320 217 lineto
-311 221 lineto
+newpath 310 215 moveto
+320 215 lineto
+311 219 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Protectedtoplevel -> Vernac
-newpath 419 198 moveto
-438 195 458 190 475 187 curveto
+newpath 419 196 moveto
+438 193 458 188 475 185 curveto
 stroke
-newpath 474 185 moveto
-484 186 lineto
-474 190 lineto
+newpath 474 183 moveto
+484 184 lineto
+474 188 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Errors
 gsave 10 dict begin
-513 234 27 18 ellipse_path
+513 232 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-513 235 moveto (Errors) 34 14.00 -0.50 alignedtext
+513 233 moveto (Errors) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Protectedtoplevel -> Errors
-newpath 419 216 moveto
-439 219 460 224 478 227 curveto
-stroke
-newpath 477 224 moveto
-486 229 lineto
-476 229 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Record
-gsave 10 dict begin
-645 18 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-645 19 moveto (Record) 40 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Record -> Class
-newpath 670 29 moveto
-678 33 686 38 692 42 curveto
-704 50 721 65 734 76 curveto
-stroke
-newpath 735 74 moveto
-741 82 lineto
-732 77 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Metasyntax
-gsave 10 dict begin
-865 97 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-865 98 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Class -> Metasyntax
-newpath 784 97 moveto
-792 97 802 97 812 97 curveto
+newpath 419 214 moveto
+439 217 460 222 478 225 curveto
 stroke
-newpath 812 95 moveto
-822 97 lineto
-812 100 lineto
+newpath 477 222 moveto
+486 227 lineto
+476 227 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Errors -> Himsg
-newpath 541 231 moveto
-584 225 669 215 718 209 curveto
+newpath 540 229 moveto
+587 224 681 214 732 208 curveto
 stroke
-newpath 718 207 moveto
-728 208 lineto
-718 211 lineto
+newpath 729 206 moveto
+739 207 lineto
+729 211 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Minicoq
 gsave 10 dict begin
-34 288 34 18 ellipse_path
+34 286 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-34 289 moveto (Minicoq) 47 14.00 -0.50 alignedtext
+34 287 moveto (Minicoq) 47 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Fhimsg
 gsave 10 dict begin
-136 288 31 18 ellipse_path
+136 286 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 289 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
+136 287 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Minicoq -> Fhimsg
-newpath 68 288 moveto
-77 288 86 288 94 288 curveto
+newpath 68 286 moveto
+77 286 86 286 94 286 curveto
 stroke
-newpath 94 286 moveto
-104 288 lineto
-94 291 lineto
+newpath 94 284 moveto
+104 286 lineto
+94 289 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqtop
 gsave 10 dict begin
-34 207 31 18 ellipse_path
+34 205 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-34 208 moveto (Coqtop) 41 14.00 -0.50 alignedtext
+34 206 moveto (Coqtop) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqinit
 gsave 10 dict begin
-136 234 31 18 ellipse_path
+136 232 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 235 moveto (Coqinit) 42 14.00 -0.50 alignedtext
+136 233 moveto (Coqinit) 42 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqtop -> Coqinit
-newpath 62 215 moveto
-73 218 86 221 98 224 curveto
+newpath 62 213 moveto
+73 216 86 219 98 222 curveto
 stroke
-newpath 98 221 moveto
-107 227 lineto
-97 226 lineto
+newpath 98 219 moveto
+107 225 lineto
+97 224 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Usage
 gsave 10 dict begin
-136 180 27 18 ellipse_path
+136 178 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-136 181 moveto (Usage) 34 14.00 -0.50 alignedtext
+136 179 moveto (Usage) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqtop -> Usage
-newpath 62 199 moveto
-74 196 88 192 101 189 curveto
+newpath 62 197 moveto
+74 194 88 190 101 187 curveto
 stroke
-newpath 100 187 moveto
-110 187 lineto
-101 192 lineto
+newpath 100 185 moveto
+110 185 lineto
+101 190 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqinit -> Toplevel
-newpath 168 234 moveto
-176 234 185 234 194 234 curveto
+newpath 168 232 moveto
+176 232 185 232 194 232 curveto
 stroke
-newpath 194 232 moveto
-204 234 lineto
-194 237 lineto
+newpath 194 230 moveto
+204 232 lineto
+194 235 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage